YES 8.323 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ LR

mainModule List
  ((group :: (Eq a, Eq b) => [(b,a)]  ->  [[(b,a)]]) :: (Eq b, Eq a) => [(b,a)]  ->  [[(b,a)]])

module List where
  import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy _ [] = []
groupBy eq (x : xs) = 
(x : ys) : groupBy eq zs where 
vv10 = span (eq x) xs
ys = (\(ys,_) ->ys) vv10
zs = (\(_,zs) ->zs) vv10


module Maybe where
  import qualified List
import qualified Prelude


Lambda Reductions:
The following Lambda expression
\(_,zs)→zs

is transformed to
zs0 (_,zs) = zs

The following Lambda expression
\(ys,_)→ys

is transformed to
ys0 (ys,_) = ys

The following Lambda expression
\(_,zs)→zs

is transformed to
zs1 (_,zs) = zs

The following Lambda expression
\(ys,_)→ys

is transformed to
ys1 (ys,_) = ys



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR

mainModule List
  ((group :: (Eq a, Eq b) => [(a,b)]  ->  [[(a,b)]]) :: (Eq b, Eq a) => [(a,b)]  ->  [[(a,b)]])

module List where
  import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy _ [] = []
groupBy eq (x : xs) = 
(x : ys) : groupBy eq zs where 
vv10 = span (eq x) xs
ys = ys0 vv10
ys0 (ys,_) = ys
zs = zs0 vv10
zs0 (_,zs) = zs


module Maybe where
  import qualified List
import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
xs@(ww : wx)

is replaced by the following term
ww : wx



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR

mainModule List
  ((group :: (Eq b, Eq a) => [(b,a)]  ->  [[(b,a)]]) :: (Eq a, Eq b) => [(b,a)]  ->  [[(b,a)]])

module List where
  import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy vw [] = []
groupBy eq (x : xs) = 
(x : ys) : groupBy eq zs where 
vv10 = span (eq x) xs
ys = ys0 vv10
ys0 (ys,vx) = ys
zs = zs0 vv10
zs0 (vy,zs) = zs


module Maybe where
  import qualified List
import qualified Prelude


Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
span p [] = ([],[])
span p (ww : wx)
 | p ww
 = (ww : ys,zs)
 | otherwise
 = ([],ww : wx)
where 
vu43  = span p wx
ys  = ys1 vu43
ys1 (ys,wz) = ys
zs  = zs1 vu43
zs1 (wy,zs) = zs

is transformed to
span p [] = span3 p []
span p (ww : wx) = span2 p (ww : wx)

span2 p (ww : wx) = 
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys1 vu43
ys1 (ys,wz) = ys
zs  = zs1 vu43
zs1 (wy,zs) = zs

span3 p [] = ([],[])
span3 yz zu = span2 yz zu



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed

mainModule List
  ((group :: (Eq b, Eq a) => [(a,b)]  ->  [[(a,b)]]) :: (Eq b, Eq a) => [(a,b)]  ->  [[(a,b)]])

module List where
  import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy vw [] = []
groupBy eq (x : xs) = 
(x : ys) : groupBy eq zs where 
vv10 = span (eq x) xs
ys = ys0 vv10
ys0 (ys,vx) = ys
zs = zs0 vv10
zs0 (vy,zs) = zs


module Maybe where
  import qualified List
import qualified Prelude


Let/Where Reductions:
The bindings of the following Let/Where expression
(x : ys) : groupBy eq zs
where 
vv10  = span (eq x) xs
ys  = ys0 vv10
ys0 (ys,vx) = ys
zs  = zs0 vv10
zs0 (vy,zs) = zs

are unpacked to the following functions on top level
groupByZs0 zv zw zx (vy,zs) = zs

groupByYs zv zw zx = groupByYs0 zv zw zx (groupByVv10 zv zw zx)

groupByZs zv zw zx = groupByZs0 zv zw zx (groupByVv10 zv zw zx)

groupByVv10 zv zw zx = span (zv zw) zx

groupByYs0 zv zw zx (ys,vx) = ys

The bindings of the following Let/Where expression
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys1 vu43
ys1 (ys,wz) = ys
zs  = zs1 vu43
zs1 (wy,zs) = zs

are unpacked to the following functions on top level
span2Vu43 zy zz = span zy zz

span2Ys zy zz = span2Ys1 zy zz (span2Vu43 zy zz)

span2Zs1 zy zz (wy,zs) = zs

span2Span1 zy zz p ww wx True = (ww : span2Ys zy zz,span2Zs zy zz)
span2Span1 zy zz p ww wx False = span2Span0 zy zz p ww wx otherwise

span2Ys1 zy zz (ys,wz) = ys

span2Span0 zy zz p ww wx True = ([],ww : wx)

span2Zs zy zz = span2Zs1 zy zz (span2Vu43 zy zz)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow

mainModule List
  (group :: (Eq a, Eq b) => [(a,b)]  ->  [[(a,b)]])

module List where
  import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy vw [] = []
groupBy eq (x : xs) = (x : groupByYs eq x xs) : groupBy eq (groupByZs eq x xs)

  
groupByVv10 zv zw zx = span (zv zw) zx

  
groupByYs zv zw zx = groupByYs0 zv zw zx (groupByVv10 zv zw zx)

  
groupByYs0 zv zw zx (ys,vx) = ys

  
groupByZs zv zw zx = groupByZs0 zv zw zx (groupByVv10 zv zw zx)

  
groupByZs0 zv zw zx (vy,zs) = zs


module Maybe where
  import qualified List
import qualified Prelude


Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vuu7500), Succ(vuu31010000)) → new_primPlusNat(vuu7500, vuu31010000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vuu301000), Succ(vuu3101000)) → new_primMulNat(vuu301000, Succ(vuu3101000))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(vuu30100), Succ(vuu310100)) → new_primEqNat(vuu30100, vuu310100)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs(Right(vuu3010), Right(vuu31010), cc, app(app(app(ty_@3, dc), dd), de)) → new_esEs3(vuu3010, vuu31010, dc, dd, de)
new_esEs3(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), baf, app(ty_Maybe, bcg), bcc) → new_esEs2(vuu3011, vuu31011, bcg)
new_esEs3(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), baf, bag, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs3(vuu3012, vuu31012, bbf, bbg, bbh)
new_esEs3(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), app(app(ty_Either, bdc), bdd), bag, bcc) → new_esEs(vuu3010, vuu31010, bdc, bdd)
new_esEs2(Just(vuu3010), Just(vuu31010), app(app(ty_Either, he), hf)) → new_esEs(vuu3010, vuu31010, he, hf)
new_esEs3(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), app(app(ty_@2, bde), bdf), bag, bcc) → new_esEs0(vuu3010, vuu31010, bde, bdf)
new_esEs(Right(vuu3010), Right(vuu31010), cc, app(ty_[], da)) → new_esEs1(vuu3010, vuu31010, da)
new_esEs3(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), baf, bag, app(ty_[], bbd)) → new_esEs1(vuu3012, vuu31012, bbd)
new_esEs1(:(vuu3010, vuu3011), :(vuu31010, vuu31011), gc) → new_esEs1(vuu3011, vuu31011, gc)
new_esEs0(@2(vuu3010, vuu3011), @2(vuu31010, vuu31011), app(ty_[], ff), fb) → new_esEs1(vuu3010, vuu31010, ff)
new_esEs3(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), baf, bag, app(app(ty_Either, bah), bba)) → new_esEs(vuu3012, vuu31012, bah, bba)
new_esEs1(:(vuu3010, vuu3011), :(vuu31010, vuu31011), app(ty_[], gh)) → new_esEs1(vuu3010, vuu31010, gh)
new_esEs3(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), baf, app(ty_[], bcf), bcc) → new_esEs1(vuu3011, vuu31011, bcf)
new_esEs2(Just(vuu3010), Just(vuu31010), app(ty_[], baa)) → new_esEs1(vuu3010, vuu31010, baa)
new_esEs(Right(vuu3010), Right(vuu31010), cc, app(app(ty_@2, cf), cg)) → new_esEs0(vuu3010, vuu31010, cf, cg)
new_esEs2(Just(vuu3010), Just(vuu31010), app(ty_Maybe, bab)) → new_esEs2(vuu3010, vuu31010, bab)
new_esEs0(@2(vuu3010, vuu3011), @2(vuu31010, vuu31011), app(app(ty_Either, eh), fa), fb) → new_esEs(vuu3010, vuu31010, eh, fa)
new_esEs3(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), baf, app(app(ty_@2, bcd), bce), bcc) → new_esEs0(vuu3011, vuu31011, bcd, bce)
new_esEs(Left(vuu3010), Left(vuu31010), app(ty_Maybe, bg), bc) → new_esEs2(vuu3010, vuu31010, bg)
new_esEs0(@2(vuu3010, vuu3011), @2(vuu31010, vuu31011), df, app(app(ty_Either, dg), dh)) → new_esEs(vuu3011, vuu31011, dg, dh)
new_esEs(Left(vuu3010), Left(vuu31010), app(app(app(ty_@3, bh), ca), cb), bc) → new_esEs3(vuu3010, vuu31010, bh, ca, cb)
new_esEs3(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), baf, app(app(app(ty_@3, bch), bda), bdb), bcc) → new_esEs3(vuu3011, vuu31011, bch, bda, bdb)
new_esEs0(@2(vuu3010, vuu3011), @2(vuu31010, vuu31011), df, app(ty_Maybe, ed)) → new_esEs2(vuu3011, vuu31011, ed)
new_esEs(Right(vuu3010), Right(vuu31010), cc, app(app(ty_Either, cd), ce)) → new_esEs(vuu3010, vuu31010, cd, ce)
new_esEs0(@2(vuu3010, vuu3011), @2(vuu31010, vuu31011), app(app(app(ty_@3, fh), ga), gb), fb) → new_esEs3(vuu3010, vuu31010, fh, ga, gb)
new_esEs(Left(vuu3010), Left(vuu31010), app(app(ty_@2, bd), be), bc) → new_esEs0(vuu3010, vuu31010, bd, be)
new_esEs1(:(vuu3010, vuu3011), :(vuu31010, vuu31011), app(ty_Maybe, ha)) → new_esEs2(vuu3010, vuu31010, ha)
new_esEs0(@2(vuu3010, vuu3011), @2(vuu31010, vuu31011), app(ty_Maybe, fg), fb) → new_esEs2(vuu3010, vuu31010, fg)
new_esEs3(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), baf, app(app(ty_Either, bca), bcb), bcc) → new_esEs(vuu3011, vuu31011, bca, bcb)
new_esEs1(:(vuu3010, vuu3011), :(vuu31010, vuu31011), app(app(app(ty_@3, hb), hc), hd)) → new_esEs3(vuu3010, vuu31010, hb, hc, hd)
new_esEs3(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), baf, bag, app(ty_Maybe, bbe)) → new_esEs2(vuu3012, vuu31012, bbe)
new_esEs3(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), app(ty_Maybe, bdh), bag, bcc) → new_esEs2(vuu3010, vuu31010, bdh)
new_esEs0(@2(vuu3010, vuu3011), @2(vuu31010, vuu31011), app(app(ty_@2, fc), fd), fb) → new_esEs0(vuu3010, vuu31010, fc, fd)
new_esEs(Right(vuu3010), Right(vuu31010), cc, app(ty_Maybe, db)) → new_esEs2(vuu3010, vuu31010, db)
new_esEs(Left(vuu3010), Left(vuu31010), app(ty_[], bf), bc) → new_esEs1(vuu3010, vuu31010, bf)
new_esEs3(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), app(ty_[], bdg), bag, bcc) → new_esEs1(vuu3010, vuu31010, bdg)
new_esEs0(@2(vuu3010, vuu3011), @2(vuu31010, vuu31011), df, app(ty_[], ec)) → new_esEs1(vuu3011, vuu31011, ec)
new_esEs2(Just(vuu3010), Just(vuu31010), app(app(app(ty_@3, bac), bad), bae)) → new_esEs3(vuu3010, vuu31010, bac, bad, bae)
new_esEs0(@2(vuu3010, vuu3011), @2(vuu31010, vuu31011), df, app(app(ty_@2, ea), eb)) → new_esEs0(vuu3011, vuu31011, ea, eb)
new_esEs1(:(vuu3010, vuu3011), :(vuu31010, vuu31011), app(app(ty_Either, gd), ge)) → new_esEs(vuu3010, vuu31010, gd, ge)
new_esEs3(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), baf, bag, app(app(ty_@2, bbb), bbc)) → new_esEs0(vuu3012, vuu31012, bbb, bbc)
new_esEs0(@2(vuu3010, vuu3011), @2(vuu31010, vuu31011), df, app(app(app(ty_@3, ee), ef), eg)) → new_esEs3(vuu3011, vuu31011, ee, ef, eg)
new_esEs1(:(vuu3010, vuu3011), :(vuu31010, vuu31011), app(app(ty_@2, gf), gg)) → new_esEs0(vuu3010, vuu31010, gf, gg)
new_esEs(Left(vuu3010), Left(vuu31010), app(app(ty_Either, ba), bb), bc) → new_esEs(vuu3010, vuu31010, ba, bb)
new_esEs3(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), app(app(app(ty_@3, bea), beb), bec), bag, bcc) → new_esEs3(vuu3010, vuu31010, bea, beb, bec)
new_esEs2(Just(vuu3010), Just(vuu31010), app(app(ty_@2, hg), hh)) → new_esEs0(vuu3010, vuu31010, hg, hh)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Ys1(vuu37, vuu38, vuu410, vuu411, True, ba, bb) → new_span2Zs(vuu37, vuu38, vuu411, ba, bb)
new_span2Zs1(vuu57, vuu58, vuu610, vuu611, True, bc, bd) → new_span2Ys(vuu57, vuu58, vuu611, bc, bd)
new_span2Zs(vuu57, vuu58, :(vuu610, vuu611), bc, bd) → new_span2Zs1(vuu57, vuu58, vuu610, vuu611, new_esEs4(@2(vuu57, vuu58), vuu610, bc, bd), bc, bd)
new_span2Ys1(vuu37, vuu38, vuu410, vuu411, True, ba, bb) → new_span2Ys(vuu37, vuu38, vuu411, ba, bb)
new_span2Ys(vuu37, vuu38, :(vuu410, vuu411), ba, bb) → new_span2Ys1(vuu37, vuu38, vuu410, vuu411, new_esEs4(@2(vuu37, vuu38), vuu410, ba, bb), ba, bb)
new_span2Zs1(vuu57, vuu58, vuu610, vuu611, True, bc, bd) → new_span2Zs(vuu57, vuu58, vuu611, bc, bd)

The TRS R consists of the following rules:

new_esEs9(vuu3010, vuu31010, app(ty_Maybe, dh)) → new_esEs17(vuu3010, vuu31010, dh)
new_esEs25(vuu3010, vuu31010, ty_Char) → new_esEs19(vuu3010, vuu31010)
new_esEs22(vuu3012, vuu31012, ty_Integer) → new_esEs14(vuu3012, vuu31012)
new_esEs22(vuu3012, vuu31012, app(ty_Ratio, fd)) → new_esEs13(vuu3012, vuu31012, fd)
new_primPlusNat1(Succ(vuu7500), Succ(vuu31010000)) → Succ(Succ(new_primPlusNat1(vuu7500, vuu31010000)))
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Double, bde) → new_esEs12(vuu3010, vuu31010)
new_esEs25(vuu3010, vuu31010, app(ty_[], bbe)) → new_esEs16(vuu3010, vuu31010, bbe)
new_primEqInt(Neg(Succ(vuu30100)), Pos(vuu31010)) → False
new_primEqInt(Pos(Succ(vuu30100)), Neg(vuu31010)) → False
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_esEs24(vuu3010, vuu31010, app(ty_Ratio, baa)) → new_esEs13(vuu3010, vuu31010, baa)
new_esEs24(vuu3010, vuu31010, app(app(ty_@2, hg), hh)) → new_esEs4(vuu3010, vuu31010, hg, hh)
new_esEs22(vuu3012, vuu31012, ty_Ordering) → new_esEs15(vuu3012, vuu31012)
new_esEs11(Right(vuu3010), Right(vuu31010), beh, ty_Ordering) → new_esEs15(vuu3010, vuu31010)
new_esEs9(vuu3010, vuu31010, ty_Float) → new_esEs6(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, app(app(ty_@2, ge), gf)) → new_esEs4(vuu3011, vuu31011, ge, gf)
new_esEs9(vuu3010, vuu31010, app(app(ty_Either, db), dc)) → new_esEs11(vuu3010, vuu31010, db, dc)
new_esEs16(:(vuu3010, vuu3011), :(vuu31010, vuu31011), bag) → new_asAs(new_esEs25(vuu3010, vuu31010, bag), new_esEs16(vuu3011, vuu31011, bag))
new_primEqInt(Pos(Zero), Neg(Succ(vuu310100))) → False
new_primEqInt(Neg(Zero), Pos(Succ(vuu310100))) → False
new_esEs21(vuu3010, vuu31010, ty_Int) → new_esEs7(vuu3010, vuu31010)
new_esEs15(EQ, EQ) → True
new_esEs23(vuu3011, vuu31011, app(ty_Maybe, ha)) → new_esEs17(vuu3011, vuu31011, ha)
new_esEs25(vuu3010, vuu31010, app(ty_Maybe, bbf)) → new_esEs17(vuu3010, vuu31010, bbf)
new_esEs24(vuu3010, vuu31010, app(ty_Maybe, bac)) → new_esEs17(vuu3010, vuu31010, bac)
new_esEs11(Right(vuu3010), Right(vuu31010), beh, ty_Char) → new_esEs19(vuu3010, vuu31010)
new_esEs8(vuu3011, vuu31011, ty_@0) → new_esEs5(vuu3011, vuu31011)
new_esEs17(Just(vuu3010), Just(vuu31010), app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs18(vuu3010, vuu31010, bdb, bdc, bdd)
new_esEs24(vuu3010, vuu31010, app(app(app(ty_@3, bad), bae), baf)) → new_esEs18(vuu3010, vuu31010, bad, bae, baf)
new_primMulNat0(Zero, Zero) → Zero
new_esEs11(Right(vuu3010), Right(vuu31010), beh, app(app(app(ty_@3, bfh), bga), bgb)) → new_esEs18(vuu3010, vuu31010, bfh, bga, bgb)
new_esEs25(vuu3010, vuu31010, ty_Double) → new_esEs12(vuu3010, vuu31010)
new_esEs25(vuu3010, vuu31010, ty_Bool) → new_esEs10(vuu3010, vuu31010)
new_esEs17(Just(vuu3010), Just(vuu31010), app(app(ty_@2, bce), bcf)) → new_esEs4(vuu3010, vuu31010, bce, bcf)
new_esEs21(vuu3010, vuu31010, ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, app(ty_Ratio, gg)) → new_esEs13(vuu3011, vuu31011, gg)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_@0, bde) → new_esEs5(vuu3010, vuu31010)
new_esEs9(vuu3010, vuu31010, ty_Bool) → new_esEs10(vuu3010, vuu31010)
new_esEs9(vuu3010, vuu31010, app(app(app(ty_@3, ea), eb), ec)) → new_esEs18(vuu3010, vuu31010, ea, eb, ec)
new_esEs25(vuu3010, vuu31010, app(app(ty_@2, bbb), bbc)) → new_esEs4(vuu3010, vuu31010, bbb, bbc)
new_esEs11(Right(vuu3010), Right(vuu31010), beh, app(app(ty_@2, bfc), bfd)) → new_esEs4(vuu3010, vuu31010, bfc, bfd)
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Float) → new_esEs6(vuu3010, vuu31010)
new_primPlusNat0(Zero, vuu3101000) → Succ(vuu3101000)
new_esEs8(vuu3011, vuu31011, ty_Float) → new_esEs6(vuu3011, vuu31011)
new_esEs8(vuu3011, vuu31011, ty_Double) → new_esEs12(vuu3011, vuu31011)
new_esEs25(vuu3010, vuu31010, ty_Int) → new_esEs7(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, ty_Int) → new_esEs7(vuu3011, vuu31011)
new_sr(Neg(vuu30100), Pos(vuu310100)) → Neg(new_primMulNat0(vuu30100, vuu310100))
new_sr(Pos(vuu30100), Neg(vuu310100)) → Neg(new_primMulNat0(vuu30100, vuu310100))
new_esEs8(vuu3011, vuu31011, app(app(app(ty_@3, cf), cg), da)) → new_esEs18(vuu3011, vuu31011, cf, cg, da)
new_esEs22(vuu3012, vuu31012, ty_Bool) → new_esEs10(vuu3012, vuu31012)
new_esEs11(Right(vuu3010), Right(vuu31010), beh, app(app(ty_Either, bfa), bfb)) → new_esEs11(vuu3010, vuu31010, bfa, bfb)
new_esEs11(Left(vuu3010), Left(vuu31010), app(app(app(ty_@3, bee), bef), beg), bde) → new_esEs18(vuu3010, vuu31010, bee, bef, beg)
new_esEs22(vuu3012, vuu31012, app(ty_[], ff)) → new_esEs16(vuu3012, vuu31012, ff)
new_esEs11(Right(vuu3010), Right(vuu31010), beh, app(ty_Maybe, bfg)) → new_esEs17(vuu3010, vuu31010, bfg)
new_esEs23(vuu3011, vuu31011, ty_Ordering) → new_esEs15(vuu3011, vuu31011)
new_esEs11(Left(vuu3010), Left(vuu31010), app(ty_[], bec), bde) → new_esEs16(vuu3010, vuu31010, bec)
new_esEs9(vuu3010, vuu31010, ty_Ordering) → new_esEs15(vuu3010, vuu31010)
new_esEs10(True, True) → True
new_esEs8(vuu3011, vuu31011, app(app(ty_@2, ca), cb)) → new_esEs4(vuu3011, vuu31011, ca, cb)
new_esEs22(vuu3012, vuu31012, ty_@0) → new_esEs5(vuu3012, vuu31012)
new_esEs11(Left(vuu3010), Left(vuu31010), app(app(ty_Either, bdf), bdg), bde) → new_esEs11(vuu3010, vuu31010, bdf, bdg)
new_esEs9(vuu3010, vuu31010, app(ty_Ratio, df)) → new_esEs13(vuu3010, vuu31010, df)
new_primEqNat0(Zero, Succ(vuu310100)) → False
new_primEqNat0(Succ(vuu30100), Zero) → False
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Double) → new_esEs12(vuu3010, vuu31010)
new_esEs15(LT, GT) → False
new_esEs15(GT, LT) → False
new_esEs23(vuu3011, vuu31011, app(app(app(ty_@3, hb), hc), hd)) → new_esEs18(vuu3011, vuu31011, hb, hc, hd)
new_esEs9(vuu3010, vuu31010, ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs5(@0, @0) → True
new_esEs15(LT, LT) → True
new_esEs20(vuu3011, vuu31011, ty_Int) → new_esEs7(vuu3011, vuu31011)
new_esEs16([], :(vuu31010, vuu31011), bag) → False
new_esEs16(:(vuu3010, vuu3011), [], bag) → False
new_esEs22(vuu3012, vuu31012, ty_Int) → new_esEs7(vuu3012, vuu31012)
new_esEs22(vuu3012, vuu31012, app(app(ty_@2, fb), fc)) → new_esEs4(vuu3012, vuu31012, fb, fc)
new_esEs11(Right(vuu3010), Right(vuu31010), beh, ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_esEs24(vuu3010, vuu31010, ty_Int) → new_esEs7(vuu3010, vuu31010)
new_esEs9(vuu3010, vuu31010, ty_@0) → new_esEs5(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, app(app(ty_Either, gc), gd)) → new_esEs11(vuu3011, vuu31011, gc, gd)
new_esEs11(Right(vuu3010), Right(vuu31010), beh, app(ty_[], bff)) → new_esEs16(vuu3010, vuu31010, bff)
new_esEs25(vuu3010, vuu31010, ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_esEs15(LT, EQ) → False
new_esEs15(EQ, LT) → False
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Integer, bde) → new_esEs14(vuu3010, vuu31010)
new_esEs14(Integer(vuu3010), Integer(vuu31010)) → new_primEqInt(vuu3010, vuu31010)
new_esEs8(vuu3011, vuu31011, ty_Ordering) → new_esEs15(vuu3011, vuu31011)
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Char) → new_esEs19(vuu3010, vuu31010)
new_esEs6(Float(vuu3010, vuu3011), Float(vuu31010, vuu31011)) → new_esEs7(new_sr(vuu3010, vuu31010), new_sr(vuu3011, vuu31011))
new_esEs19(Char(vuu3010), Char(vuu31010)) → new_primEqNat0(vuu3010, vuu31010)
new_esEs22(vuu3012, vuu31012, ty_Char) → new_esEs19(vuu3012, vuu31012)
new_esEs15(EQ, GT) → False
new_esEs15(GT, EQ) → False
new_esEs9(vuu3010, vuu31010, app(app(ty_@2, dd), de)) → new_esEs4(vuu3010, vuu31010, dd, de)
new_esEs25(vuu3010, vuu31010, ty_@0) → new_esEs5(vuu3010, vuu31010)
new_esEs25(vuu3010, vuu31010, ty_Float) → new_esEs6(vuu3010, vuu31010)
new_esEs11(Right(vuu3010), Right(vuu31010), beh, ty_Double) → new_esEs12(vuu3010, vuu31010)
new_sr(Neg(vuu30100), Neg(vuu310100)) → Pos(new_primMulNat0(vuu30100, vuu310100))
new_esEs24(vuu3010, vuu31010, ty_Double) → new_esEs12(vuu3010, vuu31010)
new_esEs11(Right(vuu3010), Right(vuu31010), beh, ty_Bool) → new_esEs10(vuu3010, vuu31010)
new_esEs25(vuu3010, vuu31010, app(ty_Ratio, bbd)) → new_esEs13(vuu3010, vuu31010, bbd)
new_esEs18(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), ee, ef, eg) → new_asAs(new_esEs24(vuu3010, vuu31010, ee), new_asAs(new_esEs23(vuu3011, vuu31011, ef), new_esEs22(vuu3012, vuu31012, eg)))
new_asAs(False, vuu68) → False
new_sr(Pos(vuu30100), Pos(vuu310100)) → Pos(new_primMulNat0(vuu30100, vuu310100))
new_esEs22(vuu3012, vuu31012, ty_Double) → new_esEs12(vuu3012, vuu31012)
new_esEs11(Right(vuu3010), Right(vuu31010), beh, ty_Int) → new_esEs7(vuu3010, vuu31010)
new_esEs11(Left(vuu3010), Left(vuu31010), app(ty_Ratio, beb), bde) → new_esEs13(vuu3010, vuu31010, beb)
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Int) → new_esEs7(vuu3010, vuu31010)
new_primEqNat0(Zero, Zero) → True
new_esEs8(vuu3011, vuu31011, ty_Integer) → new_esEs14(vuu3011, vuu31011)
new_primMulNat0(Succ(vuu301000), Zero) → Zero
new_primMulNat0(Zero, Succ(vuu3101000)) → Zero
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Char, bde) → new_esEs19(vuu3010, vuu31010)
new_esEs17(Just(vuu3010), Just(vuu31010), app(ty_Ratio, bcg)) → new_esEs13(vuu3010, vuu31010, bcg)
new_esEs8(vuu3011, vuu31011, app(ty_[], cd)) → new_esEs16(vuu3011, vuu31011, cd)
new_esEs7(vuu301, vuu3101) → new_primEqInt(vuu301, vuu3101)
new_esEs23(vuu3011, vuu31011, ty_Float) → new_esEs6(vuu3011, vuu31011)
new_esEs24(vuu3010, vuu31010, app(ty_[], bab)) → new_esEs16(vuu3010, vuu31010, bab)
new_esEs8(vuu3011, vuu31011, ty_Int) → new_esEs7(vuu3011, vuu31011)
new_esEs24(vuu3010, vuu31010, ty_@0) → new_esEs5(vuu3010, vuu31010)
new_esEs22(vuu3012, vuu31012, ty_Float) → new_esEs6(vuu3012, vuu31012)
new_esEs24(vuu3010, vuu31010, ty_Ordering) → new_esEs15(vuu3010, vuu31010)
new_esEs17(Just(vuu3010), Just(vuu31010), app(app(ty_Either, bcc), bcd)) → new_esEs11(vuu3010, vuu31010, bcc, bcd)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Bool, bde) → new_esEs10(vuu3010, vuu31010)
new_esEs9(vuu3010, vuu31010, app(ty_[], dg)) → new_esEs16(vuu3010, vuu31010, dg)
new_esEs22(vuu3012, vuu31012, app(ty_Maybe, fg)) → new_esEs17(vuu3012, vuu31012, fg)
new_esEs8(vuu3011, vuu31011, ty_Bool) → new_esEs10(vuu3011, vuu31011)
new_esEs24(vuu3010, vuu31010, ty_Char) → new_esEs19(vuu3010, vuu31010)
new_primPlusNat0(Succ(vuu750), vuu3101000) → Succ(Succ(new_primPlusNat1(vuu750, vuu3101000)))
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Ordering) → new_esEs15(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, ty_Bool) → new_esEs10(vuu3011, vuu31011)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Ordering, bde) → new_esEs15(vuu3010, vuu31010)
new_esEs20(vuu3011, vuu31011, ty_Integer) → new_esEs14(vuu3011, vuu31011)
new_esEs25(vuu3010, vuu31010, app(app(app(ty_@3, bbg), bbh), bca)) → new_esEs18(vuu3010, vuu31010, bbg, bbh, bca)
new_esEs24(vuu3010, vuu31010, ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_esEs11(Left(vuu3010), Left(vuu31010), app(ty_Maybe, bed), bde) → new_esEs17(vuu3010, vuu31010, bed)
new_primEqInt(Neg(Succ(vuu30100)), Neg(Succ(vuu310100))) → new_primEqNat0(vuu30100, vuu310100)
new_esEs11(Left(vuu3010), Left(vuu31010), app(app(ty_@2, bdh), bea), bde) → new_esEs4(vuu3010, vuu31010, bdh, bea)
new_primPlusNat1(Succ(vuu7500), Zero) → Succ(vuu7500)
new_primPlusNat1(Zero, Succ(vuu31010000)) → Succ(vuu31010000)
new_esEs16([], [], bag) → True
new_esEs24(vuu3010, vuu31010, ty_Float) → new_esEs6(vuu3010, vuu31010)
new_esEs9(vuu3010, vuu31010, ty_Int) → new_esEs7(vuu3010, vuu31010)
new_esEs17(Just(vuu3010), Just(vuu31010), app(ty_[], bch)) → new_esEs16(vuu3010, vuu31010, bch)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs24(vuu3010, vuu31010, ty_Bool) → new_esEs10(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, ty_Char) → new_esEs19(vuu3011, vuu31011)
new_esEs13(:%(vuu3010, vuu3011), :%(vuu31010, vuu31011), ed) → new_asAs(new_esEs21(vuu3010, vuu31010, ed), new_esEs20(vuu3011, vuu31011, ed))
new_esEs11(Right(vuu3010), Right(vuu31010), beh, ty_Float) → new_esEs6(vuu3010, vuu31010)
new_esEs8(vuu3011, vuu31011, app(ty_Ratio, cc)) → new_esEs13(vuu3011, vuu31011, cc)
new_primEqInt(Neg(Succ(vuu30100)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(vuu310100))) → False
new_esEs17(Nothing, Nothing, bcb) → True
new_esEs8(vuu3011, vuu31011, app(app(ty_Either, bg), bh)) → new_esEs11(vuu3011, vuu31011, bg, bh)
new_esEs23(vuu3011, vuu31011, ty_Double) → new_esEs12(vuu3011, vuu31011)
new_esEs4(@2(vuu3010, vuu3011), @2(vuu31010, vuu31011), be, bf) → new_asAs(new_esEs9(vuu3010, vuu31010, be), new_esEs8(vuu3011, vuu31011, bf))
new_esEs25(vuu3010, vuu31010, app(app(ty_Either, bah), bba)) → new_esEs11(vuu3010, vuu31010, bah, bba)
new_esEs23(vuu3011, vuu31011, app(ty_[], gh)) → new_esEs16(vuu3011, vuu31011, gh)
new_esEs10(False, False) → True
new_primPlusNat1(Zero, Zero) → Zero
new_esEs9(vuu3010, vuu31010, ty_Char) → new_esEs19(vuu3010, vuu31010)
new_asAs(True, vuu68) → vuu68
new_esEs23(vuu3011, vuu31011, ty_Integer) → new_esEs14(vuu3011, vuu31011)
new_esEs8(vuu3011, vuu31011, ty_Char) → new_esEs19(vuu3011, vuu31011)
new_primMulNat0(Succ(vuu301000), Succ(vuu3101000)) → new_primPlusNat0(new_primMulNat0(vuu301000, Succ(vuu3101000)), vuu3101000)
new_esEs10(True, False) → False
new_esEs10(False, True) → False
new_primEqInt(Pos(Succ(vuu30100)), Pos(Succ(vuu310100))) → new_primEqNat0(vuu30100, vuu310100)
new_esEs22(vuu3012, vuu31012, app(app(ty_Either, eh), fa)) → new_esEs11(vuu3012, vuu31012, eh, fa)
new_esEs17(Just(vuu3010), Nothing, bcb) → False
new_esEs17(Nothing, Just(vuu31010), bcb) → False
new_primEqNat0(Succ(vuu30100), Succ(vuu310100)) → new_primEqNat0(vuu30100, vuu310100)
new_esEs11(Right(vuu3010), Right(vuu31010), beh, app(ty_Ratio, bfe)) → new_esEs13(vuu3010, vuu31010, bfe)
new_esEs15(GT, GT) → True
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Bool) → new_esEs10(vuu3010, vuu31010)
new_esEs17(Just(vuu3010), Just(vuu31010), app(ty_Maybe, bda)) → new_esEs17(vuu3010, vuu31010, bda)
new_esEs25(vuu3010, vuu31010, ty_Ordering) → new_esEs15(vuu3010, vuu31010)
new_esEs12(Double(vuu3010, vuu3011), Double(vuu31010, vuu31011)) → new_esEs7(new_sr(vuu3010, vuu31010), new_sr(vuu3011, vuu31011))
new_esEs24(vuu3010, vuu31010, app(app(ty_Either, he), hf)) → new_esEs11(vuu3010, vuu31010, he, hf)
new_esEs17(Just(vuu3010), Just(vuu31010), ty_@0) → new_esEs5(vuu3010, vuu31010)
new_primEqInt(Pos(Zero), Pos(Succ(vuu310100))) → False
new_primEqInt(Pos(Succ(vuu30100)), Pos(Zero)) → False
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Int, bde) → new_esEs7(vuu3010, vuu31010)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs9(vuu3010, vuu31010, ty_Double) → new_esEs12(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, ty_@0) → new_esEs5(vuu3011, vuu31011)
new_esEs8(vuu3011, vuu31011, app(ty_Maybe, ce)) → new_esEs17(vuu3011, vuu31011, ce)
new_esEs11(Right(vuu3010), Right(vuu31010), beh, ty_@0) → new_esEs5(vuu3010, vuu31010)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Float, bde) → new_esEs6(vuu3010, vuu31010)
new_esEs22(vuu3012, vuu31012, app(app(app(ty_@3, fh), ga), gb)) → new_esEs18(vuu3012, vuu31012, fh, ga, gb)
new_esEs11(Right(vuu3010), Left(vuu31010), beh, bde) → False
new_esEs11(Left(vuu3010), Right(vuu31010), beh, bde) → False

The set Q consists of the following terms:

new_esEs21(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Double)
new_esEs5(@0, @0)
new_esEs8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr(Neg(x0), Neg(x1))
new_esEs11(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs23(x0, x1, ty_Float)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs4(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs24(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs22(x0, x1, ty_Bool)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_@0)
new_esEs17(Just(x0), Just(x1), ty_Double)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs20(x0, x1, ty_Int)
new_esEs16(:(x0, x1), :(x2, x3), x4)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, ty_Bool)
new_esEs8(x0, x1, ty_Int)
new_asAs(False, x0)
new_esEs8(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs9(x0, x1, ty_@0)
new_esEs11(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs22(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_primEqNat0(Succ(x0), Zero)
new_esEs11(Right(x0), Right(x1), x2, ty_Double)
new_esEs23(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs25(x0, x1, ty_@0)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs6(Float(x0, x1), Float(x2, x3))
new_esEs11(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_sr(Pos(x0), Pos(x1))
new_esEs24(x0, x1, ty_Int)
new_esEs7(x0, x1)
new_esEs23(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Float)
new_esEs9(x0, x1, ty_Ordering)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs25(x0, x1, ty_Ordering)
new_esEs9(x0, x1, ty_Double)
new_esEs11(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs9(x0, x1, ty_Char)
new_primMulNat0(Zero, Succ(x0))
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs11(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs11(Right(x0), Right(x1), x2, ty_Integer)
new_esEs16(:(x0, x1), [], x2)
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs19(Char(x0), Char(x1))
new_esEs16([], [], x0)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs13(:%(x0, x1), :%(x2, x3), x4)
new_esEs8(x0, x1, ty_Bool)
new_esEs11(Left(x0), Left(x1), ty_Bool, x2)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs11(Right(x0), Right(x1), x2, ty_Bool)
new_esEs20(x0, x1, ty_Integer)
new_esEs8(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(Left(x0), Left(x1), ty_Float, x2)
new_esEs16([], :(x0, x1), x2)
new_esEs10(False, False)
new_esEs17(Just(x0), Nothing, x1)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs11(Right(x0), Right(x1), x2, ty_Char)
new_esEs8(x0, x1, ty_@0)
new_primEqNat0(Zero, Zero)
new_esEs23(x0, x1, ty_Integer)
new_esEs11(Left(x0), Left(x1), ty_Integer, x2)
new_esEs17(Nothing, Just(x0), x1)
new_primPlusNat1(Succ(x0), Zero)
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs25(x0, x1, ty_Double)
new_esEs17(Nothing, Nothing, x0)
new_esEs8(x0, x1, ty_Double)
new_esEs15(GT, GT)
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs24(x0, x1, ty_Char)
new_esEs11(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs15(LT, GT)
new_esEs15(GT, LT)
new_primMulNat0(Succ(x0), Zero)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Zero, Zero)
new_esEs11(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs8(x0, x1, ty_Ordering)
new_esEs10(False, True)
new_esEs10(True, False)
new_esEs11(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs8(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Char)
new_esEs11(Right(x0), Right(x1), x2, ty_Int)
new_esEs22(x0, x1, ty_Int)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs11(Right(x0), Left(x1), x2, x3)
new_esEs11(Left(x0), Right(x1), x2, x3)
new_esEs24(x0, x1, ty_Double)
new_esEs11(Left(x0), Left(x1), ty_Int, x2)
new_esEs15(EQ, EQ)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(True, x0)
new_esEs24(x0, x1, ty_Float)
new_esEs11(Left(x0), Left(x1), ty_Char, x2)
new_esEs8(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Char)
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs11(Left(x0), Left(x1), ty_@0, x2)
new_esEs8(x0, x1, ty_Float)
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Char)
new_esEs22(x0, x1, ty_Integer)
new_esEs11(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(ty_[], x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs17(Just(x0), Just(x1), ty_Char)
new_esEs11(Left(x0), Left(x1), ty_Double, x2)
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs14(Integer(x0), Integer(x1))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs11(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat1(Zero, Zero)
new_primEqNat0(Zero, Succ(x0))
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs10(True, True)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs23(x0, x1, ty_Double)
new_esEs15(LT, EQ)
new_esEs15(EQ, LT)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs12(Double(x0, x1), Double(x2, x3))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs9(x0, x1, ty_Float)
new_esEs8(x0, x1, ty_Integer)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(x0, x1, app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_@0)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs15(LT, LT)
new_esEs11(Right(x0), Right(x1), x2, ty_Float)
new_esEs8(x0, x1, ty_Char)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs15(EQ, GT)
new_esEs15(GT, EQ)
new_primPlusNat1(Zero, Succ(x0))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs9(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Bool)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_groupBy(:(vuu30, vuu31), ba, bb) → new_groupBy(new_groupByZs0(vuu30, vuu31, ba, bb), ba, bb)

The TRS R consists of the following rules:

new_esEs9(vuu3010, vuu31010, app(ty_Maybe, dh)) → new_esEs17(vuu3010, vuu31010, dh)
new_esEs25(vuu3010, vuu31010, ty_Char) → new_esEs19(vuu3010, vuu31010)
new_esEs22(vuu3012, vuu31012, ty_Integer) → new_esEs14(vuu3012, vuu31012)
new_esEs22(vuu3012, vuu31012, app(ty_Ratio, fc)) → new_esEs13(vuu3012, vuu31012, fc)
new_esEs27(vuu300, vuu3100, app(ty_[], bcb)) → new_esEs16(vuu300, vuu3100, bcb)
new_esEs27(vuu300, vuu3100, ty_Char) → new_esEs19(vuu300, vuu3100)
new_primPlusNat1(Succ(vuu7500), Succ(vuu31010000)) → Succ(Succ(new_primPlusNat1(vuu7500, vuu31010000)))
new_esEs25(vuu3010, vuu31010, app(ty_[], bdd)) → new_esEs16(vuu3010, vuu31010, bdd)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Double, bba) → new_esEs12(vuu3010, vuu31010)
new_primEqInt(Neg(Succ(vuu30100)), Pos(vuu31010)) → False
new_primEqInt(Pos(Succ(vuu30100)), Neg(vuu31010)) → False
new_esEs24(vuu3010, vuu31010, app(ty_Ratio, hh)) → new_esEs13(vuu3010, vuu31010, hh)
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_esEs22(vuu3012, vuu31012, ty_Ordering) → new_esEs15(vuu3012, vuu31012)
new_esEs24(vuu3010, vuu31010, app(app(ty_@2, hf), hg)) → new_esEs4(vuu3010, vuu31010, hf, hg)
new_esEs27(vuu300, vuu3100, ty_Double) → new_esEs12(vuu300, vuu3100)
new_esEs9(vuu3010, vuu31010, ty_Float) → new_esEs6(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, app(app(ty_@2, gd), ge)) → new_esEs4(vuu3011, vuu31011, gd, ge)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_Ordering) → new_esEs15(vuu3010, vuu31010)
new_esEs9(vuu3010, vuu31010, app(app(ty_Either, db), dc)) → new_esEs11(vuu3010, vuu31010, db, dc)
new_esEs16(:(vuu3010, vuu3011), :(vuu31010, vuu31011), bbc) → new_asAs(new_esEs25(vuu3010, vuu31010, bbc), new_esEs16(vuu3011, vuu31011, bbc))
new_esEs21(vuu3010, vuu31010, ty_Int) → new_esEs7(vuu3010, vuu31010)
new_primEqInt(Neg(Zero), Pos(Succ(vuu310100))) → False
new_primEqInt(Pos(Zero), Neg(Succ(vuu310100))) → False
new_esEs15(EQ, EQ) → True
new_esEs23(vuu3011, vuu31011, app(ty_Maybe, gh)) → new_esEs17(vuu3011, vuu31011, gh)
new_esEs25(vuu3010, vuu31010, app(ty_Maybe, bde)) → new_esEs17(vuu3010, vuu31010, bde)
new_esEs24(vuu3010, vuu31010, app(ty_Maybe, bab)) → new_esEs17(vuu3010, vuu31010, bab)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_Char) → new_esEs19(vuu3010, vuu31010)
new_esEs8(vuu3011, vuu31011, ty_@0) → new_esEs5(vuu3011, vuu31011)
new_esEs24(vuu3010, vuu31010, app(app(app(ty_@3, bac), bad), bae)) → new_esEs18(vuu3010, vuu31010, bac, bad, bae)
new_esEs17(Just(vuu3010), Just(vuu31010), app(app(app(ty_@3, beh), bfa), bfb)) → new_esEs18(vuu3010, vuu31010, beh, bfa, bfb)
new_primMulNat0(Zero, Zero) → Zero
new_esEs11(Right(vuu3010), Right(vuu31010), bah, app(app(app(ty_@3, bhd), bhe), bhf)) → new_esEs18(vuu3010, vuu31010, bhd, bhe, bhf)
new_esEs25(vuu3010, vuu31010, ty_Double) → new_esEs12(vuu3010, vuu31010)
new_esEs25(vuu3010, vuu31010, ty_Bool) → new_esEs10(vuu3010, vuu31010)
new_esEs17(Just(vuu3010), Just(vuu31010), app(app(ty_@2, bec), bed)) → new_esEs4(vuu3010, vuu31010, bec, bed)
new_esEs26(vuu301, vuu3101, app(ty_[], bbc)) → new_esEs16(vuu301, vuu3101, bbc)
new_esEs21(vuu3010, vuu31010, ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, app(ty_Ratio, gf)) → new_esEs13(vuu3011, vuu31011, gf)
new_esEs9(vuu3010, vuu31010, ty_Bool) → new_esEs10(vuu3010, vuu31010)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_@0, bba) → new_esEs5(vuu3010, vuu31010)
new_esEs9(vuu3010, vuu31010, app(app(app(ty_@3, ea), eb), ec)) → new_esEs18(vuu3010, vuu31010, ea, eb, ec)
new_esEs25(vuu3010, vuu31010, app(app(ty_@2, bda), bdb)) → new_esEs4(vuu3010, vuu31010, bda, bdb)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, app(app(ty_@2, bgg), bgh)) → new_esEs4(vuu3010, vuu31010, bgg, bgh)
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Float) → new_esEs6(vuu3010, vuu31010)
new_primPlusNat0(Zero, vuu3101000) → Succ(vuu3101000)
new_esEs8(vuu3011, vuu31011, ty_Float) → new_esEs6(vuu3011, vuu31011)
new_esEs27(vuu300, vuu3100, app(ty_Maybe, bcc)) → new_esEs17(vuu300, vuu3100, bcc)
new_esEs8(vuu3011, vuu31011, ty_Double) → new_esEs12(vuu3011, vuu31011)
new_esEs26(vuu301, vuu3101, app(app(app(ty_@3, ed), ee), ef)) → new_esEs18(vuu301, vuu3101, ed, ee, ef)
new_span2Ys10(vuu37, vuu38, vuu410, vuu411, False, baf, bag) → []
new_esEs25(vuu3010, vuu31010, ty_Int) → new_esEs7(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, ty_Int) → new_esEs7(vuu3011, vuu31011)
new_esEs26(vuu301, vuu3101, ty_Float) → new_esEs6(vuu301, vuu3101)
new_sr(Neg(vuu30100), Pos(vuu310100)) → Neg(new_primMulNat0(vuu30100, vuu310100))
new_sr(Pos(vuu30100), Neg(vuu310100)) → Neg(new_primMulNat0(vuu30100, vuu310100))
new_esEs8(vuu3011, vuu31011, app(app(app(ty_@3, cf), cg), da)) → new_esEs18(vuu3011, vuu31011, cf, cg, da)
new_groupByZs00(vuu57, vuu58, vuu59, vuu60, vuu61, True, bc, bd) → new_span2Zs0(vuu57, vuu58, vuu61, bc, bd)
new_esEs22(vuu3012, vuu31012, ty_Bool) → new_esEs10(vuu3012, vuu31012)
new_esEs27(vuu300, vuu3100, ty_@0) → new_esEs5(vuu300, vuu3100)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, app(app(ty_Either, bge), bgf)) → new_esEs11(vuu3010, vuu31010, bge, bgf)
new_esEs11(Left(vuu3010), Left(vuu31010), app(app(app(ty_@3, bgb), bgc), bgd), bba) → new_esEs18(vuu3010, vuu31010, bgb, bgc, bgd)
new_esEs27(vuu300, vuu3100, ty_Bool) → new_esEs10(vuu300, vuu3100)
new_esEs22(vuu3012, vuu31012, app(ty_[], fd)) → new_esEs16(vuu3012, vuu31012, fd)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, app(ty_Maybe, bhc)) → new_esEs17(vuu3010, vuu31010, bhc)
new_esEs23(vuu3011, vuu31011, ty_Ordering) → new_esEs15(vuu3011, vuu31011)
new_esEs9(vuu3010, vuu31010, ty_Ordering) → new_esEs15(vuu3010, vuu31010)
new_esEs11(Left(vuu3010), Left(vuu31010), app(ty_[], bfh), bba) → new_esEs16(vuu3010, vuu31010, bfh)
new_esEs10(True, True) → True
new_esEs27(vuu300, vuu3100, app(app(ty_Either, bbe), bbf)) → new_esEs11(vuu300, vuu3100, bbe, bbf)
new_esEs26(vuu301, vuu3101, ty_Integer) → new_esEs14(vuu301, vuu3101)
new_esEs8(vuu3011, vuu31011, app(app(ty_@2, ca), cb)) → new_esEs4(vuu3011, vuu31011, ca, cb)
new_esEs22(vuu3012, vuu31012, ty_@0) → new_esEs5(vuu3012, vuu31012)
new_esEs11(Left(vuu3010), Left(vuu31010), app(app(ty_Either, bfc), bfd), bba) → new_esEs11(vuu3010, vuu31010, bfc, bfd)
new_esEs9(vuu3010, vuu31010, app(ty_Ratio, df)) → new_esEs13(vuu3010, vuu31010, df)
new_esEs26(vuu301, vuu3101, ty_@0) → new_esEs5(vuu301, vuu3101)
new_primEqNat0(Succ(vuu30100), Zero) → False
new_primEqNat0(Zero, Succ(vuu310100)) → False
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Double) → new_esEs12(vuu3010, vuu31010)
new_esEs15(GT, LT) → False
new_esEs15(LT, GT) → False
new_esEs23(vuu3011, vuu31011, app(app(app(ty_@3, ha), hb), hc)) → new_esEs18(vuu3011, vuu31011, ha, hb, hc)
new_esEs9(vuu3010, vuu31010, ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs26(vuu301, vuu3101, ty_Bool) → new_esEs10(vuu301, vuu3101)
new_groupByZs0(vuu30, [], ba, bb) → []
new_groupByZs0(@2(vuu300, vuu301), :(@2(vuu3100, vuu3101), vuu311), ba, bb) → new_groupByZs00(vuu300, vuu301, vuu3100, vuu3101, vuu311, new_asAs(new_esEs27(vuu300, vuu3100, ba), new_esEs26(vuu301, vuu3101, bb)), ba, bb)
new_esEs5(@0, @0) → True
new_esEs20(vuu3011, vuu31011, ty_Int) → new_esEs7(vuu3011, vuu31011)
new_esEs26(vuu301, vuu3101, app(app(ty_Either, bah), bba)) → new_esEs11(vuu301, vuu3101, bah, bba)
new_esEs15(LT, LT) → True
new_esEs16([], :(vuu31010, vuu31011), bbc) → False
new_esEs16(:(vuu3010, vuu3011), [], bbc) → False
new_esEs22(vuu3012, vuu31012, ty_Int) → new_esEs7(vuu3012, vuu31012)
new_esEs27(vuu300, vuu3100, ty_Ordering) → new_esEs15(vuu300, vuu3100)
new_esEs22(vuu3012, vuu31012, app(app(ty_@2, fa), fb)) → new_esEs4(vuu3012, vuu31012, fa, fb)
new_esEs26(vuu301, vuu3101, ty_Ordering) → new_esEs15(vuu301, vuu3101)
new_esEs24(vuu3010, vuu31010, ty_Int) → new_esEs7(vuu3010, vuu31010)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_esEs9(vuu3010, vuu31010, ty_@0) → new_esEs5(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, app(app(ty_Either, gb), gc)) → new_esEs11(vuu3011, vuu31011, gb, gc)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, app(ty_[], bhb)) → new_esEs16(vuu3010, vuu31010, bhb)
new_esEs25(vuu3010, vuu31010, ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_esEs15(EQ, LT) → False
new_esEs15(LT, EQ) → False
new_esEs14(Integer(vuu3010), Integer(vuu31010)) → new_primEqInt(vuu3010, vuu31010)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Integer, bba) → new_esEs14(vuu3010, vuu31010)
new_esEs26(vuu301, vuu3101, ty_Char) → new_esEs19(vuu301, vuu3101)
new_span2Ys11(vuu37, vuu38, vuu410, vuu411, vuu72, vuu71, baf, bag) → :(vuu410, vuu72)
new_esEs8(vuu3011, vuu31011, ty_Ordering) → new_esEs15(vuu3011, vuu31011)
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Char) → new_esEs19(vuu3010, vuu31010)
new_groupByZs00(vuu57, vuu58, vuu59, vuu60, vuu61, False, bc, bd) → :(@2(vuu59, vuu60), vuu61)
new_esEs26(vuu301, vuu3101, ty_Double) → new_esEs12(vuu301, vuu3101)
new_esEs6(Float(vuu3010, vuu3011), Float(vuu31010, vuu31011)) → new_esEs7(new_sr(vuu3010, vuu31010), new_sr(vuu3011, vuu31011))
new_esEs19(Char(vuu3010), Char(vuu31010)) → new_primEqNat0(vuu3010, vuu31010)
new_esEs22(vuu3012, vuu31012, ty_Char) → new_esEs19(vuu3012, vuu31012)
new_esEs15(GT, EQ) → False
new_esEs15(EQ, GT) → False
new_esEs9(vuu3010, vuu31010, app(app(ty_@2, dd), de)) → new_esEs4(vuu3010, vuu31010, dd, de)
new_esEs25(vuu3010, vuu31010, ty_@0) → new_esEs5(vuu3010, vuu31010)
new_esEs25(vuu3010, vuu31010, ty_Float) → new_esEs6(vuu3010, vuu31010)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_Double) → new_esEs12(vuu3010, vuu31010)
new_sr(Neg(vuu30100), Neg(vuu310100)) → Pos(new_primMulNat0(vuu30100, vuu310100))
new_esEs27(vuu300, vuu3100, ty_Int) → new_esEs7(vuu300, vuu3100)
new_esEs24(vuu3010, vuu31010, ty_Double) → new_esEs12(vuu3010, vuu31010)
new_span2Ys0(vuu37, vuu38, [], baf, bag) → []
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_Bool) → new_esEs10(vuu3010, vuu31010)
new_esEs25(vuu3010, vuu31010, app(ty_Ratio, bdc)) → new_esEs13(vuu3010, vuu31010, bdc)
new_esEs18(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), ed, ee, ef) → new_asAs(new_esEs24(vuu3010, vuu31010, ed), new_asAs(new_esEs23(vuu3011, vuu31011, ee), new_esEs22(vuu3012, vuu31012, ef)))
new_sr(Pos(vuu30100), Pos(vuu310100)) → Pos(new_primMulNat0(vuu30100, vuu310100))
new_asAs(False, vuu68) → False
new_esEs22(vuu3012, vuu31012, ty_Double) → new_esEs12(vuu3012, vuu31012)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_Int) → new_esEs7(vuu3010, vuu31010)
new_esEs11(Left(vuu3010), Left(vuu31010), app(ty_Ratio, bfg), bba) → new_esEs13(vuu3010, vuu31010, bfg)
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Int) → new_esEs7(vuu3010, vuu31010)
new_primEqNat0(Zero, Zero) → True
new_primMulNat0(Zero, Succ(vuu3101000)) → Zero
new_primMulNat0(Succ(vuu301000), Zero) → Zero
new_esEs8(vuu3011, vuu31011, ty_Integer) → new_esEs14(vuu3011, vuu31011)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Char, bba) → new_esEs19(vuu3010, vuu31010)
new_esEs17(Just(vuu3010), Just(vuu31010), app(ty_Ratio, bee)) → new_esEs13(vuu3010, vuu31010, bee)
new_esEs8(vuu3011, vuu31011, app(ty_[], cd)) → new_esEs16(vuu3011, vuu31011, cd)
new_esEs7(vuu301, vuu3101) → new_primEqInt(vuu301, vuu3101)
new_esEs26(vuu301, vuu3101, app(ty_Ratio, bbb)) → new_esEs13(vuu301, vuu3101, bbb)
new_esEs23(vuu3011, vuu31011, ty_Float) → new_esEs6(vuu3011, vuu31011)
new_esEs8(vuu3011, vuu31011, ty_Int) → new_esEs7(vuu3011, vuu31011)
new_esEs24(vuu3010, vuu31010, app(ty_[], baa)) → new_esEs16(vuu3010, vuu31010, baa)
new_esEs27(vuu300, vuu3100, app(ty_Ratio, bca)) → new_esEs13(vuu300, vuu3100, bca)
new_esEs24(vuu3010, vuu31010, ty_@0) → new_esEs5(vuu3010, vuu31010)
new_esEs27(vuu300, vuu3100, ty_Float) → new_esEs6(vuu300, vuu3100)
new_esEs22(vuu3012, vuu31012, ty_Float) → new_esEs6(vuu3012, vuu31012)
new_esEs24(vuu3010, vuu31010, ty_Ordering) → new_esEs15(vuu3010, vuu31010)
new_esEs17(Just(vuu3010), Just(vuu31010), app(app(ty_Either, bea), beb)) → new_esEs11(vuu3010, vuu31010, bea, beb)
new_esEs26(vuu301, vuu3101, app(ty_Maybe, bbd)) → new_esEs17(vuu301, vuu3101, bbd)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Bool, bba) → new_esEs10(vuu3010, vuu31010)
new_esEs9(vuu3010, vuu31010, app(ty_[], dg)) → new_esEs16(vuu3010, vuu31010, dg)
new_esEs26(vuu301, vuu3101, ty_Int) → new_esEs7(vuu301, vuu3101)
new_esEs22(vuu3012, vuu31012, app(ty_Maybe, ff)) → new_esEs17(vuu3012, vuu31012, ff)
new_esEs8(vuu3011, vuu31011, ty_Bool) → new_esEs10(vuu3011, vuu31011)
new_esEs24(vuu3010, vuu31010, ty_Char) → new_esEs19(vuu3010, vuu31010)
new_primPlusNat0(Succ(vuu750), vuu3101000) → Succ(Succ(new_primPlusNat1(vuu750, vuu3101000)))
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Ordering) → new_esEs15(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, ty_Bool) → new_esEs10(vuu3011, vuu31011)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Ordering, bba) → new_esEs15(vuu3010, vuu31010)
new_esEs20(vuu3011, vuu31011, ty_Integer) → new_esEs14(vuu3011, vuu31011)
new_span2Zs11(vuu57, vuu58, vuu610, vuu611, False, bc, bd) → :(vuu610, vuu611)
new_esEs25(vuu3010, vuu31010, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs18(vuu3010, vuu31010, bdf, bdg, bdh)
new_esEs24(vuu3010, vuu31010, ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_esEs27(vuu300, vuu3100, app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs18(vuu300, vuu3100, bcd, bce, bcf)
new_span2Zs0(vuu57, vuu58, [], bc, bd) → []
new_esEs11(Left(vuu3010), Left(vuu31010), app(ty_Maybe, bga), bba) → new_esEs17(vuu3010, vuu31010, bga)
new_primEqInt(Neg(Succ(vuu30100)), Neg(Succ(vuu310100))) → new_primEqNat0(vuu30100, vuu310100)
new_esEs11(Left(vuu3010), Left(vuu31010), app(app(ty_@2, bfe), bff), bba) → new_esEs4(vuu3010, vuu31010, bfe, bff)
new_esEs27(vuu300, vuu3100, app(app(ty_@2, bbg), bbh)) → new_esEs4(vuu300, vuu3100, bbg, bbh)
new_primPlusNat1(Zero, Succ(vuu31010000)) → Succ(vuu31010000)
new_primPlusNat1(Succ(vuu7500), Zero) → Succ(vuu7500)
new_span2Zs11(vuu57, vuu58, vuu610, vuu611, True, bc, bd) → new_span2Zs10(vuu57, vuu58, vuu610, vuu611, new_span2Ys0(vuu57, vuu58, vuu611, bc, bd), new_span2Zs0(vuu57, vuu58, vuu611, bc, bd), bc, bd)
new_esEs16([], [], bbc) → True
new_esEs24(vuu3010, vuu31010, ty_Float) → new_esEs6(vuu3010, vuu31010)
new_span2Zs10(vuu57, vuu58, vuu610, vuu611, vuu74, vuu73, bc, bd) → vuu73
new_esEs9(vuu3010, vuu31010, ty_Int) → new_esEs7(vuu3010, vuu31010)
new_esEs17(Just(vuu3010), Just(vuu31010), app(ty_[], bef)) → new_esEs16(vuu3010, vuu31010, bef)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs23(vuu3011, vuu31011, ty_Char) → new_esEs19(vuu3011, vuu31011)
new_esEs24(vuu3010, vuu31010, ty_Bool) → new_esEs10(vuu3010, vuu31010)
new_esEs13(:%(vuu3010, vuu3011), :%(vuu31010, vuu31011), bbb) → new_asAs(new_esEs21(vuu3010, vuu31010, bbb), new_esEs20(vuu3011, vuu31011, bbb))
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_Float) → new_esEs6(vuu3010, vuu31010)
new_esEs8(vuu3011, vuu31011, app(ty_Ratio, cc)) → new_esEs13(vuu3011, vuu31011, cc)
new_primEqInt(Neg(Zero), Neg(Succ(vuu310100))) → False
new_primEqInt(Neg(Succ(vuu30100)), Neg(Zero)) → False
new_esEs17(Nothing, Nothing, bbd) → True
new_esEs8(vuu3011, vuu31011, app(app(ty_Either, bg), bh)) → new_esEs11(vuu3011, vuu31011, bg, bh)
new_span2Ys10(vuu37, vuu38, vuu410, vuu411, True, baf, bag) → new_span2Ys11(vuu37, vuu38, vuu410, vuu411, new_span2Ys0(vuu37, vuu38, vuu411, baf, bag), new_span2Zs0(vuu37, vuu38, vuu411, baf, bag), baf, bag)
new_esEs23(vuu3011, vuu31011, ty_Double) → new_esEs12(vuu3011, vuu31011)
new_esEs4(@2(vuu3010, vuu3011), @2(vuu31010, vuu31011), be, bf) → new_asAs(new_esEs9(vuu3010, vuu31010, be), new_esEs8(vuu3011, vuu31011, bf))
new_esEs25(vuu3010, vuu31010, app(app(ty_Either, bcg), bch)) → new_esEs11(vuu3010, vuu31010, bcg, bch)
new_esEs23(vuu3011, vuu31011, app(ty_[], gg)) → new_esEs16(vuu3011, vuu31011, gg)
new_esEs10(False, False) → True
new_primPlusNat1(Zero, Zero) → Zero
new_esEs9(vuu3010, vuu31010, ty_Char) → new_esEs19(vuu3010, vuu31010)
new_esEs27(vuu300, vuu3100, ty_Integer) → new_esEs14(vuu300, vuu3100)
new_span2Ys0(vuu37, vuu38, :(vuu410, vuu411), baf, bag) → new_span2Ys10(vuu37, vuu38, vuu410, vuu411, new_esEs4(@2(vuu37, vuu38), vuu410, baf, bag), baf, bag)
new_asAs(True, vuu68) → vuu68
new_esEs23(vuu3011, vuu31011, ty_Integer) → new_esEs14(vuu3011, vuu31011)
new_esEs8(vuu3011, vuu31011, ty_Char) → new_esEs19(vuu3011, vuu31011)
new_primMulNat0(Succ(vuu301000), Succ(vuu3101000)) → new_primPlusNat0(new_primMulNat0(vuu301000, Succ(vuu3101000)), vuu3101000)
new_esEs10(True, False) → False
new_esEs10(False, True) → False
new_span2Zs0(vuu57, vuu58, :(vuu610, vuu611), bc, bd) → new_span2Zs11(vuu57, vuu58, vuu610, vuu611, new_esEs4(@2(vuu57, vuu58), vuu610, bc, bd), bc, bd)
new_primEqInt(Pos(Succ(vuu30100)), Pos(Succ(vuu310100))) → new_primEqNat0(vuu30100, vuu310100)
new_esEs22(vuu3012, vuu31012, app(app(ty_Either, eg), eh)) → new_esEs11(vuu3012, vuu31012, eg, eh)
new_esEs17(Just(vuu3010), Nothing, bbd) → False
new_esEs17(Nothing, Just(vuu31010), bbd) → False
new_primEqNat0(Succ(vuu30100), Succ(vuu310100)) → new_primEqNat0(vuu30100, vuu310100)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, app(ty_Ratio, bha)) → new_esEs13(vuu3010, vuu31010, bha)
new_esEs15(GT, GT) → True
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Bool) → new_esEs10(vuu3010, vuu31010)
new_esEs17(Just(vuu3010), Just(vuu31010), app(ty_Maybe, beg)) → new_esEs17(vuu3010, vuu31010, beg)
new_esEs26(vuu301, vuu3101, app(app(ty_@2, be), bf)) → new_esEs4(vuu301, vuu3101, be, bf)
new_esEs25(vuu3010, vuu31010, ty_Ordering) → new_esEs15(vuu3010, vuu31010)
new_esEs12(Double(vuu3010, vuu3011), Double(vuu31010, vuu31011)) → new_esEs7(new_sr(vuu3010, vuu31010), new_sr(vuu3011, vuu31011))
new_esEs24(vuu3010, vuu31010, app(app(ty_Either, hd), he)) → new_esEs11(vuu3010, vuu31010, hd, he)
new_esEs17(Just(vuu3010), Just(vuu31010), ty_@0) → new_esEs5(vuu3010, vuu31010)
new_primEqInt(Pos(Zero), Pos(Succ(vuu310100))) → False
new_primEqInt(Pos(Succ(vuu30100)), Pos(Zero)) → False
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Int, bba) → new_esEs7(vuu3010, vuu31010)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs9(vuu3010, vuu31010, ty_Double) → new_esEs12(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, ty_@0) → new_esEs5(vuu3011, vuu31011)
new_esEs8(vuu3011, vuu31011, app(ty_Maybe, ce)) → new_esEs17(vuu3011, vuu31011, ce)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_@0) → new_esEs5(vuu3010, vuu31010)
new_esEs22(vuu3012, vuu31012, app(app(app(ty_@3, fg), fh), ga)) → new_esEs18(vuu3012, vuu31012, fg, fh, ga)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Float, bba) → new_esEs6(vuu3010, vuu31010)
new_esEs11(Left(vuu3010), Right(vuu31010), bah, bba) → False
new_esEs11(Right(vuu3010), Left(vuu31010), bah, bba) → False

The set Q consists of the following terms:

new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Int)
new_esEs11(Right(x0), Right(x1), x2, ty_Integer)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs9(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Double)
new_esEs5(@0, @0)
new_esEs8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_span2Ys11(x0, x1, x2, x3, x4, x5, x6, x7)
new_sr(Neg(x0), Neg(x1))
new_esEs11(Right(x0), Right(x1), x2, ty_Double)
new_esEs11(Left(x0), Left(x1), ty_Int, x2)
new_esEs23(x0, x1, ty_Float)
new_esEs4(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs27(x0, x1, ty_Bool)
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_esEs24(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs22(x0, x1, ty_Bool)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs11(Right(x0), Right(x1), x2, ty_Float)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_span2Zs10(x0, x1, x2, x3, x4, x5, x6, x7)
new_esEs11(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs17(Just(x0), Just(x1), ty_Double)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, ty_Int)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Bool)
new_esEs8(x0, x1, ty_Int)
new_esEs8(x0, x1, app(ty_Maybe, x2))
new_asAs(False, x0)
new_esEs24(x0, x1, ty_Integer)
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(x0, x1, ty_@0)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs25(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Int)
new_esEs11(Left(x0), Left(x1), ty_Integer, x2)
new_primEqNat0(Succ(x0), Zero)
new_esEs23(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_span2Ys0(x0, x1, [], x2, x3)
new_esEs16(:(x0, x1), [], x2)
new_esEs25(x0, x1, ty_@0)
new_esEs11(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs17(Just(x0), Nothing, x1)
new_groupByZs00(x0, x1, x2, x3, x4, False, x5, x6)
new_esEs6(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Pos(x0), Pos(x1))
new_esEs24(x0, x1, ty_Int)
new_esEs7(x0, x1)
new_esEs23(x0, x1, ty_Int)
new_esEs13(:%(x0, x1), :%(x2, x3), x4)
new_groupByZs00(x0, x1, x2, x3, x4, True, x5, x6)
new_esEs22(x0, x1, ty_Float)
new_esEs17(Nothing, Nothing, x0)
new_esEs9(x0, x1, ty_Ordering)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs25(x0, x1, ty_Ordering)
new_esEs9(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_Char)
new_primMulNat0(Zero, Succ(x0))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs11(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs11(Left(x0), Left(x1), ty_Char, x2)
new_esEs11(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(Char(x0), Char(x1))
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Bool)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_esEs8(x0, x1, ty_Bool)
new_esEs27(x0, x1, ty_@0)
new_esEs26(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Integer)
new_esEs8(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_span2Zs0(x0, x1, [], x2, x3)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Char)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs10(False, False)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_Bool, x2)
new_esEs8(x0, x1, ty_@0)
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs11(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs11(Left(x0), Right(x1), x2, x3)
new_esEs11(Right(x0), Left(x1), x2, x3)
new_primEqNat0(Zero, Zero)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, ty_Ordering)
new_esEs11(Right(x0), Right(x1), x2, ty_Char)
new_primPlusNat1(Succ(x0), Zero)
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs25(x0, x1, ty_Double)
new_esEs15(GT, GT)
new_esEs8(x0, x1, ty_Double)
new_esEs27(x0, x1, ty_Double)
new_esEs17(Nothing, Just(x0), x1)
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs24(x0, x1, ty_Char)
new_groupByZs0(@2(x0, x1), :(@2(x2, x3), x4), x5, x6)
new_esEs15(GT, LT)
new_esEs15(LT, GT)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs11(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs8(x0, x1, ty_Ordering)
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs11(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Float)
new_esEs16([], :(x0, x1), x2)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Double)
new_esEs15(EQ, EQ)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(True, x0)
new_esEs24(x0, x1, ty_Float)
new_esEs11(Left(x0), Left(x1), ty_Float, x2)
new_esEs8(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_span2Ys0(x0, x1, :(x2, x3), x4, x5)
new_esEs27(x0, x1, ty_Integer)
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Char)
new_esEs8(x0, x1, ty_Float)
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Char)
new_esEs22(x0, x1, ty_Integer)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat0(Succ(x0), x1)
new_esEs17(Just(x0), Just(x1), ty_Char)
new_span2Ys10(x0, x1, x2, x3, True, x4, x5)
new_esEs11(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_span2Zs11(x0, x1, x2, x3, True, x4, x5)
new_esEs11(Left(x0), Left(x1), ty_@0, x2)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs14(Integer(x0), Integer(x1))
new_esEs9(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs11(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs11(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Int)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primMulNat0(Succ(x0), Succ(x1))
new_span2Zs0(x0, x1, :(x2, x3), x4, x5)
new_primPlusNat1(Zero, Zero)
new_primEqNat0(Zero, Succ(x0))
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_Int)
new_esEs10(True, True)
new_esEs23(x0, x1, ty_Double)
new_esEs11(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs15(LT, EQ)
new_esEs15(EQ, LT)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs12(Double(x0, x1), Double(x2, x3))
new_esEs25(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_Float)
new_esEs8(x0, x1, ty_Integer)
new_span2Ys10(x0, x1, x2, x3, False, x4, x5)
new_esEs16(:(x0, x1), :(x2, x3), x4)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Right(x0), Right(x1), x2, ty_@0)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, ty_Ordering)
new_span2Zs11(x0, x1, x2, x3, False, x4, x5)
new_esEs8(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs15(LT, LT)
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs8(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primEqNat0(Succ(x0), Succ(x1))
new_groupByZs0(x0, [], x1, x2)
new_esEs26(x0, x1, ty_Integer)
new_esEs15(EQ, GT)
new_esEs15(GT, EQ)
new_primPlusNat1(Zero, Succ(x0))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16([], [], x0)
new_esEs9(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Bool)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_groupBy(:(vuu30, vuu31), ba, bb) → new_groupBy(new_groupByZs0(vuu30, vuu31, ba, bb), ba, bb)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(:(x1, x2)) = 1 + x2   
POL(:%(x1, x2)) = 0   
POL(@0) = 0   
POL(@2(x1, x2)) = 0   
POL(@3(x1, x2, x3)) = 0   
POL(Char(x1)) = 0   
POL(Double(x1, x2)) = 0   
POL(EQ) = 0   
POL(False) = 0   
POL(Float(x1, x2)) = 0   
POL(GT) = 0   
POL(Integer(x1)) = 0   
POL(Just(x1)) = 0   
POL(LT) = 0   
POL(Left(x1)) = 0   
POL(Neg(x1)) = 1   
POL(Nothing) = 0   
POL(Pos(x1)) = 1 + x1   
POL(Right(x1)) = 0   
POL(Succ(x1)) = 0   
POL(True) = 0   
POL(Zero) = 1   
POL([]) = 1   
POL(app(x1, x2)) = x2   
POL(new_asAs(x1, x2)) = 0   
POL(new_esEs10(x1, x2)) = 1   
POL(new_esEs11(x1, x2, x3, x4)) = 1   
POL(new_esEs12(x1, x2)) = 1   
POL(new_esEs13(x1, x2, x3)) = 1   
POL(new_esEs14(x1, x2)) = 1   
POL(new_esEs15(x1, x2)) = 0   
POL(new_esEs16(x1, x2, x3)) = 0   
POL(new_esEs17(x1, x2, x3)) = 0   
POL(new_esEs18(x1, x2, x3, x4, x5)) = 1   
POL(new_esEs19(x1, x2)) = 0   
POL(new_esEs20(x1, x2, x3)) = 0   
POL(new_esEs21(x1, x2, x3)) = 1 + x1 + x2   
POL(new_esEs22(x1, x2, x3)) = 0   
POL(new_esEs23(x1, x2, x3)) = 0   
POL(new_esEs24(x1, x2, x3)) = 1 + x1 + x3   
POL(new_esEs25(x1, x2, x3)) = 1 + x3   
POL(new_esEs26(x1, x2, x3)) = 0   
POL(new_esEs27(x1, x2, x3)) = 1   
POL(new_esEs4(x1, x2, x3, x4)) = 0   
POL(new_esEs5(x1, x2)) = 1   
POL(new_esEs6(x1, x2)) = 0   
POL(new_esEs7(x1, x2)) = 0   
POL(new_esEs8(x1, x2, x3)) = 0   
POL(new_esEs9(x1, x2, x3)) = 1 + x2 + x3   
POL(new_groupBy(x1, x2, x3)) = x1   
POL(new_groupByZs0(x1, x2, x3, x4)) = x2   
POL(new_groupByZs00(x1, x2, x3, x4, x5, x6, x7, x8)) = 1 + x5   
POL(new_primEqInt(x1, x2)) = 0   
POL(new_primEqNat0(x1, x2)) = 0   
POL(new_primMulNat0(x1, x2)) = 0   
POL(new_primPlusNat0(x1, x2)) = 0   
POL(new_primPlusNat1(x1, x2)) = x1 + x2   
POL(new_span2Ys0(x1, x2, x3, x4, x5)) = x3   
POL(new_span2Ys10(x1, x2, x3, x4, x5, x6, x7)) = 1 + x4   
POL(new_span2Ys11(x1, x2, x3, x4, x5, x6, x7, x8)) = 1 + x5   
POL(new_span2Zs0(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_span2Zs10(x1, x2, x3, x4, x5, x6, x7, x8)) = x6   
POL(new_span2Zs11(x1, x2, x3, x4, x5, x6, x7)) = 1 + x4   
POL(new_sr(x1, x2)) = x1 + x2   
POL(ty_@0) = 1   
POL(ty_@2) = 0   
POL(ty_@3) = 0   
POL(ty_Bool) = 0   
POL(ty_Char) = 1   
POL(ty_Double) = 1   
POL(ty_Either) = 0   
POL(ty_Float) = 0   
POL(ty_Int) = 0   
POL(ty_Integer) = 0   
POL(ty_Maybe) = 0   
POL(ty_Ordering) = 0   
POL(ty_Ratio) = 0   
POL(ty_[]) = 0   

The following usable rules [17] were oriented:

new_span2Zs11(vuu57, vuu58, vuu610, vuu611, False, bc, bd) → :(vuu610, vuu611)
new_groupByZs00(vuu57, vuu58, vuu59, vuu60, vuu61, False, bc, bd) → :(@2(vuu59, vuu60), vuu61)
new_span2Ys0(vuu37, vuu38, :(vuu410, vuu411), baf, bag) → new_span2Ys10(vuu37, vuu38, vuu410, vuu411, new_esEs4(@2(vuu37, vuu38), vuu410, baf, bag), baf, bag)
new_span2Ys11(vuu37, vuu38, vuu410, vuu411, vuu72, vuu71, baf, bag) → :(vuu410, vuu72)
new_span2Zs11(vuu57, vuu58, vuu610, vuu611, True, bc, bd) → new_span2Zs10(vuu57, vuu58, vuu610, vuu611, new_span2Ys0(vuu57, vuu58, vuu611, bc, bd), new_span2Zs0(vuu57, vuu58, vuu611, bc, bd), bc, bd)
new_span2Ys10(vuu37, vuu38, vuu410, vuu411, True, baf, bag) → new_span2Ys11(vuu37, vuu38, vuu410, vuu411, new_span2Ys0(vuu37, vuu38, vuu411, baf, bag), new_span2Zs0(vuu37, vuu38, vuu411, baf, bag), baf, bag)
new_groupByZs00(vuu57, vuu58, vuu59, vuu60, vuu61, True, bc, bd) → new_span2Zs0(vuu57, vuu58, vuu61, bc, bd)
new_span2Ys0(vuu37, vuu38, [], baf, bag) → []
new_span2Zs10(vuu57, vuu58, vuu610, vuu611, vuu74, vuu73, bc, bd) → vuu73
new_span2Ys10(vuu37, vuu38, vuu410, vuu411, False, baf, bag) → []
new_groupByZs0(vuu30, [], ba, bb) → []
new_span2Zs0(vuu57, vuu58, [], bc, bd) → []
new_span2Zs0(vuu57, vuu58, :(vuu610, vuu611), bc, bd) → new_span2Zs11(vuu57, vuu58, vuu610, vuu611, new_esEs4(@2(vuu57, vuu58), vuu610, bc, bd), bc, bd)
new_groupByZs0(@2(vuu300, vuu301), :(@2(vuu3100, vuu3101), vuu311), ba, bb) → new_groupByZs00(vuu300, vuu301, vuu3100, vuu3101, vuu311, new_asAs(new_esEs27(vuu300, vuu3100, ba), new_esEs26(vuu301, vuu3101, bb)), ba, bb)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

new_esEs9(vuu3010, vuu31010, app(ty_Maybe, dh)) → new_esEs17(vuu3010, vuu31010, dh)
new_esEs25(vuu3010, vuu31010, ty_Char) → new_esEs19(vuu3010, vuu31010)
new_esEs22(vuu3012, vuu31012, ty_Integer) → new_esEs14(vuu3012, vuu31012)
new_esEs22(vuu3012, vuu31012, app(ty_Ratio, fc)) → new_esEs13(vuu3012, vuu31012, fc)
new_esEs27(vuu300, vuu3100, app(ty_[], bcb)) → new_esEs16(vuu300, vuu3100, bcb)
new_esEs27(vuu300, vuu3100, ty_Char) → new_esEs19(vuu300, vuu3100)
new_primPlusNat1(Succ(vuu7500), Succ(vuu31010000)) → Succ(Succ(new_primPlusNat1(vuu7500, vuu31010000)))
new_esEs25(vuu3010, vuu31010, app(ty_[], bdd)) → new_esEs16(vuu3010, vuu31010, bdd)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Double, bba) → new_esEs12(vuu3010, vuu31010)
new_primEqInt(Neg(Succ(vuu30100)), Pos(vuu31010)) → False
new_primEqInt(Pos(Succ(vuu30100)), Neg(vuu31010)) → False
new_esEs24(vuu3010, vuu31010, app(ty_Ratio, hh)) → new_esEs13(vuu3010, vuu31010, hh)
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_esEs22(vuu3012, vuu31012, ty_Ordering) → new_esEs15(vuu3012, vuu31012)
new_esEs24(vuu3010, vuu31010, app(app(ty_@2, hf), hg)) → new_esEs4(vuu3010, vuu31010, hf, hg)
new_esEs27(vuu300, vuu3100, ty_Double) → new_esEs12(vuu300, vuu3100)
new_esEs9(vuu3010, vuu31010, ty_Float) → new_esEs6(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, app(app(ty_@2, gd), ge)) → new_esEs4(vuu3011, vuu31011, gd, ge)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_Ordering) → new_esEs15(vuu3010, vuu31010)
new_esEs9(vuu3010, vuu31010, app(app(ty_Either, db), dc)) → new_esEs11(vuu3010, vuu31010, db, dc)
new_esEs16(:(vuu3010, vuu3011), :(vuu31010, vuu31011), bbc) → new_asAs(new_esEs25(vuu3010, vuu31010, bbc), new_esEs16(vuu3011, vuu31011, bbc))
new_esEs21(vuu3010, vuu31010, ty_Int) → new_esEs7(vuu3010, vuu31010)
new_primEqInt(Neg(Zero), Pos(Succ(vuu310100))) → False
new_primEqInt(Pos(Zero), Neg(Succ(vuu310100))) → False
new_esEs15(EQ, EQ) → True
new_esEs23(vuu3011, vuu31011, app(ty_Maybe, gh)) → new_esEs17(vuu3011, vuu31011, gh)
new_esEs25(vuu3010, vuu31010, app(ty_Maybe, bde)) → new_esEs17(vuu3010, vuu31010, bde)
new_esEs24(vuu3010, vuu31010, app(ty_Maybe, bab)) → new_esEs17(vuu3010, vuu31010, bab)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_Char) → new_esEs19(vuu3010, vuu31010)
new_esEs8(vuu3011, vuu31011, ty_@0) → new_esEs5(vuu3011, vuu31011)
new_esEs24(vuu3010, vuu31010, app(app(app(ty_@3, bac), bad), bae)) → new_esEs18(vuu3010, vuu31010, bac, bad, bae)
new_esEs17(Just(vuu3010), Just(vuu31010), app(app(app(ty_@3, beh), bfa), bfb)) → new_esEs18(vuu3010, vuu31010, beh, bfa, bfb)
new_primMulNat0(Zero, Zero) → Zero
new_esEs11(Right(vuu3010), Right(vuu31010), bah, app(app(app(ty_@3, bhd), bhe), bhf)) → new_esEs18(vuu3010, vuu31010, bhd, bhe, bhf)
new_esEs25(vuu3010, vuu31010, ty_Double) → new_esEs12(vuu3010, vuu31010)
new_esEs25(vuu3010, vuu31010, ty_Bool) → new_esEs10(vuu3010, vuu31010)
new_esEs17(Just(vuu3010), Just(vuu31010), app(app(ty_@2, bec), bed)) → new_esEs4(vuu3010, vuu31010, bec, bed)
new_esEs26(vuu301, vuu3101, app(ty_[], bbc)) → new_esEs16(vuu301, vuu3101, bbc)
new_esEs21(vuu3010, vuu31010, ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, app(ty_Ratio, gf)) → new_esEs13(vuu3011, vuu31011, gf)
new_esEs9(vuu3010, vuu31010, ty_Bool) → new_esEs10(vuu3010, vuu31010)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_@0, bba) → new_esEs5(vuu3010, vuu31010)
new_esEs9(vuu3010, vuu31010, app(app(app(ty_@3, ea), eb), ec)) → new_esEs18(vuu3010, vuu31010, ea, eb, ec)
new_esEs25(vuu3010, vuu31010, app(app(ty_@2, bda), bdb)) → new_esEs4(vuu3010, vuu31010, bda, bdb)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, app(app(ty_@2, bgg), bgh)) → new_esEs4(vuu3010, vuu31010, bgg, bgh)
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Float) → new_esEs6(vuu3010, vuu31010)
new_primPlusNat0(Zero, vuu3101000) → Succ(vuu3101000)
new_esEs8(vuu3011, vuu31011, ty_Float) → new_esEs6(vuu3011, vuu31011)
new_esEs27(vuu300, vuu3100, app(ty_Maybe, bcc)) → new_esEs17(vuu300, vuu3100, bcc)
new_esEs8(vuu3011, vuu31011, ty_Double) → new_esEs12(vuu3011, vuu31011)
new_esEs26(vuu301, vuu3101, app(app(app(ty_@3, ed), ee), ef)) → new_esEs18(vuu301, vuu3101, ed, ee, ef)
new_span2Ys10(vuu37, vuu38, vuu410, vuu411, False, baf, bag) → []
new_esEs25(vuu3010, vuu31010, ty_Int) → new_esEs7(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, ty_Int) → new_esEs7(vuu3011, vuu31011)
new_esEs26(vuu301, vuu3101, ty_Float) → new_esEs6(vuu301, vuu3101)
new_sr(Neg(vuu30100), Pos(vuu310100)) → Neg(new_primMulNat0(vuu30100, vuu310100))
new_sr(Pos(vuu30100), Neg(vuu310100)) → Neg(new_primMulNat0(vuu30100, vuu310100))
new_esEs8(vuu3011, vuu31011, app(app(app(ty_@3, cf), cg), da)) → new_esEs18(vuu3011, vuu31011, cf, cg, da)
new_groupByZs00(vuu57, vuu58, vuu59, vuu60, vuu61, True, bc, bd) → new_span2Zs0(vuu57, vuu58, vuu61, bc, bd)
new_esEs22(vuu3012, vuu31012, ty_Bool) → new_esEs10(vuu3012, vuu31012)
new_esEs27(vuu300, vuu3100, ty_@0) → new_esEs5(vuu300, vuu3100)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, app(app(ty_Either, bge), bgf)) → new_esEs11(vuu3010, vuu31010, bge, bgf)
new_esEs11(Left(vuu3010), Left(vuu31010), app(app(app(ty_@3, bgb), bgc), bgd), bba) → new_esEs18(vuu3010, vuu31010, bgb, bgc, bgd)
new_esEs27(vuu300, vuu3100, ty_Bool) → new_esEs10(vuu300, vuu3100)
new_esEs22(vuu3012, vuu31012, app(ty_[], fd)) → new_esEs16(vuu3012, vuu31012, fd)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, app(ty_Maybe, bhc)) → new_esEs17(vuu3010, vuu31010, bhc)
new_esEs23(vuu3011, vuu31011, ty_Ordering) → new_esEs15(vuu3011, vuu31011)
new_esEs9(vuu3010, vuu31010, ty_Ordering) → new_esEs15(vuu3010, vuu31010)
new_esEs11(Left(vuu3010), Left(vuu31010), app(ty_[], bfh), bba) → new_esEs16(vuu3010, vuu31010, bfh)
new_esEs10(True, True) → True
new_esEs27(vuu300, vuu3100, app(app(ty_Either, bbe), bbf)) → new_esEs11(vuu300, vuu3100, bbe, bbf)
new_esEs26(vuu301, vuu3101, ty_Integer) → new_esEs14(vuu301, vuu3101)
new_esEs8(vuu3011, vuu31011, app(app(ty_@2, ca), cb)) → new_esEs4(vuu3011, vuu31011, ca, cb)
new_esEs22(vuu3012, vuu31012, ty_@0) → new_esEs5(vuu3012, vuu31012)
new_esEs11(Left(vuu3010), Left(vuu31010), app(app(ty_Either, bfc), bfd), bba) → new_esEs11(vuu3010, vuu31010, bfc, bfd)
new_esEs9(vuu3010, vuu31010, app(ty_Ratio, df)) → new_esEs13(vuu3010, vuu31010, df)
new_esEs26(vuu301, vuu3101, ty_@0) → new_esEs5(vuu301, vuu3101)
new_primEqNat0(Succ(vuu30100), Zero) → False
new_primEqNat0(Zero, Succ(vuu310100)) → False
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Double) → new_esEs12(vuu3010, vuu31010)
new_esEs15(GT, LT) → False
new_esEs15(LT, GT) → False
new_esEs23(vuu3011, vuu31011, app(app(app(ty_@3, ha), hb), hc)) → new_esEs18(vuu3011, vuu31011, ha, hb, hc)
new_esEs9(vuu3010, vuu31010, ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs26(vuu301, vuu3101, ty_Bool) → new_esEs10(vuu301, vuu3101)
new_groupByZs0(vuu30, [], ba, bb) → []
new_groupByZs0(@2(vuu300, vuu301), :(@2(vuu3100, vuu3101), vuu311), ba, bb) → new_groupByZs00(vuu300, vuu301, vuu3100, vuu3101, vuu311, new_asAs(new_esEs27(vuu300, vuu3100, ba), new_esEs26(vuu301, vuu3101, bb)), ba, bb)
new_esEs5(@0, @0) → True
new_esEs20(vuu3011, vuu31011, ty_Int) → new_esEs7(vuu3011, vuu31011)
new_esEs26(vuu301, vuu3101, app(app(ty_Either, bah), bba)) → new_esEs11(vuu301, vuu3101, bah, bba)
new_esEs15(LT, LT) → True
new_esEs16([], :(vuu31010, vuu31011), bbc) → False
new_esEs16(:(vuu3010, vuu3011), [], bbc) → False
new_esEs22(vuu3012, vuu31012, ty_Int) → new_esEs7(vuu3012, vuu31012)
new_esEs27(vuu300, vuu3100, ty_Ordering) → new_esEs15(vuu300, vuu3100)
new_esEs22(vuu3012, vuu31012, app(app(ty_@2, fa), fb)) → new_esEs4(vuu3012, vuu31012, fa, fb)
new_esEs26(vuu301, vuu3101, ty_Ordering) → new_esEs15(vuu301, vuu3101)
new_esEs24(vuu3010, vuu31010, ty_Int) → new_esEs7(vuu3010, vuu31010)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_esEs9(vuu3010, vuu31010, ty_@0) → new_esEs5(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, app(app(ty_Either, gb), gc)) → new_esEs11(vuu3011, vuu31011, gb, gc)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, app(ty_[], bhb)) → new_esEs16(vuu3010, vuu31010, bhb)
new_esEs25(vuu3010, vuu31010, ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_esEs15(EQ, LT) → False
new_esEs15(LT, EQ) → False
new_esEs14(Integer(vuu3010), Integer(vuu31010)) → new_primEqInt(vuu3010, vuu31010)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Integer, bba) → new_esEs14(vuu3010, vuu31010)
new_esEs26(vuu301, vuu3101, ty_Char) → new_esEs19(vuu301, vuu3101)
new_span2Ys11(vuu37, vuu38, vuu410, vuu411, vuu72, vuu71, baf, bag) → :(vuu410, vuu72)
new_esEs8(vuu3011, vuu31011, ty_Ordering) → new_esEs15(vuu3011, vuu31011)
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Char) → new_esEs19(vuu3010, vuu31010)
new_groupByZs00(vuu57, vuu58, vuu59, vuu60, vuu61, False, bc, bd) → :(@2(vuu59, vuu60), vuu61)
new_esEs26(vuu301, vuu3101, ty_Double) → new_esEs12(vuu301, vuu3101)
new_esEs6(Float(vuu3010, vuu3011), Float(vuu31010, vuu31011)) → new_esEs7(new_sr(vuu3010, vuu31010), new_sr(vuu3011, vuu31011))
new_esEs19(Char(vuu3010), Char(vuu31010)) → new_primEqNat0(vuu3010, vuu31010)
new_esEs22(vuu3012, vuu31012, ty_Char) → new_esEs19(vuu3012, vuu31012)
new_esEs15(GT, EQ) → False
new_esEs15(EQ, GT) → False
new_esEs9(vuu3010, vuu31010, app(app(ty_@2, dd), de)) → new_esEs4(vuu3010, vuu31010, dd, de)
new_esEs25(vuu3010, vuu31010, ty_@0) → new_esEs5(vuu3010, vuu31010)
new_esEs25(vuu3010, vuu31010, ty_Float) → new_esEs6(vuu3010, vuu31010)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_Double) → new_esEs12(vuu3010, vuu31010)
new_sr(Neg(vuu30100), Neg(vuu310100)) → Pos(new_primMulNat0(vuu30100, vuu310100))
new_esEs27(vuu300, vuu3100, ty_Int) → new_esEs7(vuu300, vuu3100)
new_esEs24(vuu3010, vuu31010, ty_Double) → new_esEs12(vuu3010, vuu31010)
new_span2Ys0(vuu37, vuu38, [], baf, bag) → []
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_Bool) → new_esEs10(vuu3010, vuu31010)
new_esEs25(vuu3010, vuu31010, app(ty_Ratio, bdc)) → new_esEs13(vuu3010, vuu31010, bdc)
new_esEs18(@3(vuu3010, vuu3011, vuu3012), @3(vuu31010, vuu31011, vuu31012), ed, ee, ef) → new_asAs(new_esEs24(vuu3010, vuu31010, ed), new_asAs(new_esEs23(vuu3011, vuu31011, ee), new_esEs22(vuu3012, vuu31012, ef)))
new_sr(Pos(vuu30100), Pos(vuu310100)) → Pos(new_primMulNat0(vuu30100, vuu310100))
new_asAs(False, vuu68) → False
new_esEs22(vuu3012, vuu31012, ty_Double) → new_esEs12(vuu3012, vuu31012)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_Int) → new_esEs7(vuu3010, vuu31010)
new_esEs11(Left(vuu3010), Left(vuu31010), app(ty_Ratio, bfg), bba) → new_esEs13(vuu3010, vuu31010, bfg)
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Int) → new_esEs7(vuu3010, vuu31010)
new_primEqNat0(Zero, Zero) → True
new_primMulNat0(Zero, Succ(vuu3101000)) → Zero
new_primMulNat0(Succ(vuu301000), Zero) → Zero
new_esEs8(vuu3011, vuu31011, ty_Integer) → new_esEs14(vuu3011, vuu31011)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Char, bba) → new_esEs19(vuu3010, vuu31010)
new_esEs17(Just(vuu3010), Just(vuu31010), app(ty_Ratio, bee)) → new_esEs13(vuu3010, vuu31010, bee)
new_esEs8(vuu3011, vuu31011, app(ty_[], cd)) → new_esEs16(vuu3011, vuu31011, cd)
new_esEs7(vuu301, vuu3101) → new_primEqInt(vuu301, vuu3101)
new_esEs26(vuu301, vuu3101, app(ty_Ratio, bbb)) → new_esEs13(vuu301, vuu3101, bbb)
new_esEs23(vuu3011, vuu31011, ty_Float) → new_esEs6(vuu3011, vuu31011)
new_esEs8(vuu3011, vuu31011, ty_Int) → new_esEs7(vuu3011, vuu31011)
new_esEs24(vuu3010, vuu31010, app(ty_[], baa)) → new_esEs16(vuu3010, vuu31010, baa)
new_esEs27(vuu300, vuu3100, app(ty_Ratio, bca)) → new_esEs13(vuu300, vuu3100, bca)
new_esEs24(vuu3010, vuu31010, ty_@0) → new_esEs5(vuu3010, vuu31010)
new_esEs27(vuu300, vuu3100, ty_Float) → new_esEs6(vuu300, vuu3100)
new_esEs22(vuu3012, vuu31012, ty_Float) → new_esEs6(vuu3012, vuu31012)
new_esEs24(vuu3010, vuu31010, ty_Ordering) → new_esEs15(vuu3010, vuu31010)
new_esEs17(Just(vuu3010), Just(vuu31010), app(app(ty_Either, bea), beb)) → new_esEs11(vuu3010, vuu31010, bea, beb)
new_esEs26(vuu301, vuu3101, app(ty_Maybe, bbd)) → new_esEs17(vuu301, vuu3101, bbd)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Bool, bba) → new_esEs10(vuu3010, vuu31010)
new_esEs9(vuu3010, vuu31010, app(ty_[], dg)) → new_esEs16(vuu3010, vuu31010, dg)
new_esEs26(vuu301, vuu3101, ty_Int) → new_esEs7(vuu301, vuu3101)
new_esEs22(vuu3012, vuu31012, app(ty_Maybe, ff)) → new_esEs17(vuu3012, vuu31012, ff)
new_esEs8(vuu3011, vuu31011, ty_Bool) → new_esEs10(vuu3011, vuu31011)
new_esEs24(vuu3010, vuu31010, ty_Char) → new_esEs19(vuu3010, vuu31010)
new_primPlusNat0(Succ(vuu750), vuu3101000) → Succ(Succ(new_primPlusNat1(vuu750, vuu3101000)))
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Ordering) → new_esEs15(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, ty_Bool) → new_esEs10(vuu3011, vuu31011)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Ordering, bba) → new_esEs15(vuu3010, vuu31010)
new_esEs20(vuu3011, vuu31011, ty_Integer) → new_esEs14(vuu3011, vuu31011)
new_span2Zs11(vuu57, vuu58, vuu610, vuu611, False, bc, bd) → :(vuu610, vuu611)
new_esEs25(vuu3010, vuu31010, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs18(vuu3010, vuu31010, bdf, bdg, bdh)
new_esEs24(vuu3010, vuu31010, ty_Integer) → new_esEs14(vuu3010, vuu31010)
new_esEs27(vuu300, vuu3100, app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs18(vuu300, vuu3100, bcd, bce, bcf)
new_span2Zs0(vuu57, vuu58, [], bc, bd) → []
new_esEs11(Left(vuu3010), Left(vuu31010), app(ty_Maybe, bga), bba) → new_esEs17(vuu3010, vuu31010, bga)
new_primEqInt(Neg(Succ(vuu30100)), Neg(Succ(vuu310100))) → new_primEqNat0(vuu30100, vuu310100)
new_esEs11(Left(vuu3010), Left(vuu31010), app(app(ty_@2, bfe), bff), bba) → new_esEs4(vuu3010, vuu31010, bfe, bff)
new_esEs27(vuu300, vuu3100, app(app(ty_@2, bbg), bbh)) → new_esEs4(vuu300, vuu3100, bbg, bbh)
new_primPlusNat1(Zero, Succ(vuu31010000)) → Succ(vuu31010000)
new_primPlusNat1(Succ(vuu7500), Zero) → Succ(vuu7500)
new_span2Zs11(vuu57, vuu58, vuu610, vuu611, True, bc, bd) → new_span2Zs10(vuu57, vuu58, vuu610, vuu611, new_span2Ys0(vuu57, vuu58, vuu611, bc, bd), new_span2Zs0(vuu57, vuu58, vuu611, bc, bd), bc, bd)
new_esEs16([], [], bbc) → True
new_esEs24(vuu3010, vuu31010, ty_Float) → new_esEs6(vuu3010, vuu31010)
new_span2Zs10(vuu57, vuu58, vuu610, vuu611, vuu74, vuu73, bc, bd) → vuu73
new_esEs9(vuu3010, vuu31010, ty_Int) → new_esEs7(vuu3010, vuu31010)
new_esEs17(Just(vuu3010), Just(vuu31010), app(ty_[], bef)) → new_esEs16(vuu3010, vuu31010, bef)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs23(vuu3011, vuu31011, ty_Char) → new_esEs19(vuu3011, vuu31011)
new_esEs24(vuu3010, vuu31010, ty_Bool) → new_esEs10(vuu3010, vuu31010)
new_esEs13(:%(vuu3010, vuu3011), :%(vuu31010, vuu31011), bbb) → new_asAs(new_esEs21(vuu3010, vuu31010, bbb), new_esEs20(vuu3011, vuu31011, bbb))
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_Float) → new_esEs6(vuu3010, vuu31010)
new_esEs8(vuu3011, vuu31011, app(ty_Ratio, cc)) → new_esEs13(vuu3011, vuu31011, cc)
new_primEqInt(Neg(Zero), Neg(Succ(vuu310100))) → False
new_primEqInt(Neg(Succ(vuu30100)), Neg(Zero)) → False
new_esEs17(Nothing, Nothing, bbd) → True
new_esEs8(vuu3011, vuu31011, app(app(ty_Either, bg), bh)) → new_esEs11(vuu3011, vuu31011, bg, bh)
new_span2Ys10(vuu37, vuu38, vuu410, vuu411, True, baf, bag) → new_span2Ys11(vuu37, vuu38, vuu410, vuu411, new_span2Ys0(vuu37, vuu38, vuu411, baf, bag), new_span2Zs0(vuu37, vuu38, vuu411, baf, bag), baf, bag)
new_esEs23(vuu3011, vuu31011, ty_Double) → new_esEs12(vuu3011, vuu31011)
new_esEs4(@2(vuu3010, vuu3011), @2(vuu31010, vuu31011), be, bf) → new_asAs(new_esEs9(vuu3010, vuu31010, be), new_esEs8(vuu3011, vuu31011, bf))
new_esEs25(vuu3010, vuu31010, app(app(ty_Either, bcg), bch)) → new_esEs11(vuu3010, vuu31010, bcg, bch)
new_esEs23(vuu3011, vuu31011, app(ty_[], gg)) → new_esEs16(vuu3011, vuu31011, gg)
new_esEs10(False, False) → True
new_primPlusNat1(Zero, Zero) → Zero
new_esEs9(vuu3010, vuu31010, ty_Char) → new_esEs19(vuu3010, vuu31010)
new_esEs27(vuu300, vuu3100, ty_Integer) → new_esEs14(vuu300, vuu3100)
new_span2Ys0(vuu37, vuu38, :(vuu410, vuu411), baf, bag) → new_span2Ys10(vuu37, vuu38, vuu410, vuu411, new_esEs4(@2(vuu37, vuu38), vuu410, baf, bag), baf, bag)
new_asAs(True, vuu68) → vuu68
new_esEs23(vuu3011, vuu31011, ty_Integer) → new_esEs14(vuu3011, vuu31011)
new_esEs8(vuu3011, vuu31011, ty_Char) → new_esEs19(vuu3011, vuu31011)
new_primMulNat0(Succ(vuu301000), Succ(vuu3101000)) → new_primPlusNat0(new_primMulNat0(vuu301000, Succ(vuu3101000)), vuu3101000)
new_esEs10(True, False) → False
new_esEs10(False, True) → False
new_span2Zs0(vuu57, vuu58, :(vuu610, vuu611), bc, bd) → new_span2Zs11(vuu57, vuu58, vuu610, vuu611, new_esEs4(@2(vuu57, vuu58), vuu610, bc, bd), bc, bd)
new_primEqInt(Pos(Succ(vuu30100)), Pos(Succ(vuu310100))) → new_primEqNat0(vuu30100, vuu310100)
new_esEs22(vuu3012, vuu31012, app(app(ty_Either, eg), eh)) → new_esEs11(vuu3012, vuu31012, eg, eh)
new_esEs17(Just(vuu3010), Nothing, bbd) → False
new_esEs17(Nothing, Just(vuu31010), bbd) → False
new_primEqNat0(Succ(vuu30100), Succ(vuu310100)) → new_primEqNat0(vuu30100, vuu310100)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, app(ty_Ratio, bha)) → new_esEs13(vuu3010, vuu31010, bha)
new_esEs15(GT, GT) → True
new_esEs17(Just(vuu3010), Just(vuu31010), ty_Bool) → new_esEs10(vuu3010, vuu31010)
new_esEs17(Just(vuu3010), Just(vuu31010), app(ty_Maybe, beg)) → new_esEs17(vuu3010, vuu31010, beg)
new_esEs26(vuu301, vuu3101, app(app(ty_@2, be), bf)) → new_esEs4(vuu301, vuu3101, be, bf)
new_esEs25(vuu3010, vuu31010, ty_Ordering) → new_esEs15(vuu3010, vuu31010)
new_esEs12(Double(vuu3010, vuu3011), Double(vuu31010, vuu31011)) → new_esEs7(new_sr(vuu3010, vuu31010), new_sr(vuu3011, vuu31011))
new_esEs24(vuu3010, vuu31010, app(app(ty_Either, hd), he)) → new_esEs11(vuu3010, vuu31010, hd, he)
new_esEs17(Just(vuu3010), Just(vuu31010), ty_@0) → new_esEs5(vuu3010, vuu31010)
new_primEqInt(Pos(Zero), Pos(Succ(vuu310100))) → False
new_primEqInt(Pos(Succ(vuu30100)), Pos(Zero)) → False
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Int, bba) → new_esEs7(vuu3010, vuu31010)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs9(vuu3010, vuu31010, ty_Double) → new_esEs12(vuu3010, vuu31010)
new_esEs23(vuu3011, vuu31011, ty_@0) → new_esEs5(vuu3011, vuu31011)
new_esEs8(vuu3011, vuu31011, app(ty_Maybe, ce)) → new_esEs17(vuu3011, vuu31011, ce)
new_esEs11(Right(vuu3010), Right(vuu31010), bah, ty_@0) → new_esEs5(vuu3010, vuu31010)
new_esEs22(vuu3012, vuu31012, app(app(app(ty_@3, fg), fh), ga)) → new_esEs18(vuu3012, vuu31012, fg, fh, ga)
new_esEs11(Left(vuu3010), Left(vuu31010), ty_Float, bba) → new_esEs6(vuu3010, vuu31010)
new_esEs11(Left(vuu3010), Right(vuu31010), bah, bba) → False
new_esEs11(Right(vuu3010), Left(vuu31010), bah, bba) → False

The set Q consists of the following terms:

new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Int)
new_esEs11(Right(x0), Right(x1), x2, ty_Integer)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs9(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Double)
new_esEs5(@0, @0)
new_esEs8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_span2Ys11(x0, x1, x2, x3, x4, x5, x6, x7)
new_sr(Neg(x0), Neg(x1))
new_esEs11(Right(x0), Right(x1), x2, ty_Double)
new_esEs11(Left(x0), Left(x1), ty_Int, x2)
new_esEs23(x0, x1, ty_Float)
new_esEs4(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs27(x0, x1, ty_Bool)
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_esEs24(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs22(x0, x1, ty_Bool)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs11(Right(x0), Right(x1), x2, ty_Float)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_span2Zs10(x0, x1, x2, x3, x4, x5, x6, x7)
new_esEs11(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs17(Just(x0), Just(x1), ty_Double)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, ty_Int)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Bool)
new_esEs8(x0, x1, ty_Int)
new_esEs8(x0, x1, app(ty_Maybe, x2))
new_asAs(False, x0)
new_esEs24(x0, x1, ty_Integer)
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(x0, x1, ty_@0)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs25(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Int)
new_esEs11(Left(x0), Left(x1), ty_Integer, x2)
new_primEqNat0(Succ(x0), Zero)
new_esEs23(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_span2Ys0(x0, x1, [], x2, x3)
new_esEs16(:(x0, x1), [], x2)
new_esEs25(x0, x1, ty_@0)
new_esEs11(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs17(Just(x0), Nothing, x1)
new_groupByZs00(x0, x1, x2, x3, x4, False, x5, x6)
new_esEs6(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Pos(x0), Pos(x1))
new_esEs24(x0, x1, ty_Int)
new_esEs7(x0, x1)
new_esEs23(x0, x1, ty_Int)
new_esEs13(:%(x0, x1), :%(x2, x3), x4)
new_groupByZs00(x0, x1, x2, x3, x4, True, x5, x6)
new_esEs22(x0, x1, ty_Float)
new_esEs17(Nothing, Nothing, x0)
new_esEs9(x0, x1, ty_Ordering)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs25(x0, x1, ty_Ordering)
new_esEs9(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_Char)
new_primMulNat0(Zero, Succ(x0))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs11(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs11(Left(x0), Left(x1), ty_Char, x2)
new_esEs11(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(Char(x0), Char(x1))
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Bool)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_esEs8(x0, x1, ty_Bool)
new_esEs27(x0, x1, ty_@0)
new_esEs26(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Integer)
new_esEs8(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_span2Zs0(x0, x1, [], x2, x3)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Char)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs10(False, False)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_Bool, x2)
new_esEs8(x0, x1, ty_@0)
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs11(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs11(Left(x0), Right(x1), x2, x3)
new_esEs11(Right(x0), Left(x1), x2, x3)
new_primEqNat0(Zero, Zero)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, ty_Ordering)
new_esEs11(Right(x0), Right(x1), x2, ty_Char)
new_primPlusNat1(Succ(x0), Zero)
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs25(x0, x1, ty_Double)
new_esEs15(GT, GT)
new_esEs8(x0, x1, ty_Double)
new_esEs27(x0, x1, ty_Double)
new_esEs17(Nothing, Just(x0), x1)
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs24(x0, x1, ty_Char)
new_groupByZs0(@2(x0, x1), :(@2(x2, x3), x4), x5, x6)
new_esEs15(GT, LT)
new_esEs15(LT, GT)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs11(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs8(x0, x1, ty_Ordering)
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs11(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Float)
new_esEs16([], :(x0, x1), x2)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Double)
new_esEs15(EQ, EQ)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(True, x0)
new_esEs24(x0, x1, ty_Float)
new_esEs11(Left(x0), Left(x1), ty_Float, x2)
new_esEs8(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_span2Ys0(x0, x1, :(x2, x3), x4, x5)
new_esEs27(x0, x1, ty_Integer)
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Char)
new_esEs8(x0, x1, ty_Float)
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Char)
new_esEs22(x0, x1, ty_Integer)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat0(Succ(x0), x1)
new_esEs17(Just(x0), Just(x1), ty_Char)
new_span2Ys10(x0, x1, x2, x3, True, x4, x5)
new_esEs11(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_span2Zs11(x0, x1, x2, x3, True, x4, x5)
new_esEs11(Left(x0), Left(x1), ty_@0, x2)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs14(Integer(x0), Integer(x1))
new_esEs9(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs11(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs11(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Int)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primMulNat0(Succ(x0), Succ(x1))
new_span2Zs0(x0, x1, :(x2, x3), x4, x5)
new_primPlusNat1(Zero, Zero)
new_primEqNat0(Zero, Succ(x0))
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_Int)
new_esEs10(True, True)
new_esEs23(x0, x1, ty_Double)
new_esEs11(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs15(LT, EQ)
new_esEs15(EQ, LT)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs12(Double(x0, x1), Double(x2, x3))
new_esEs25(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_Float)
new_esEs8(x0, x1, ty_Integer)
new_span2Ys10(x0, x1, x2, x3, False, x4, x5)
new_esEs16(:(x0, x1), :(x2, x3), x4)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Right(x0), Right(x1), x2, ty_@0)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, ty_Ordering)
new_span2Zs11(x0, x1, x2, x3, False, x4, x5)
new_esEs8(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs15(LT, LT)
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs8(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primEqNat0(Succ(x0), Succ(x1))
new_groupByZs0(x0, [], x1, x2)
new_esEs26(x0, x1, ty_Integer)
new_esEs15(EQ, GT)
new_esEs15(GT, EQ)
new_primPlusNat1(Zero, Succ(x0))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16([], [], x0)
new_esEs9(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Bool)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.